RequirementMachine: Preliminary design doc

Author: slavapestov

docs/RequirementMachine/Makefile

@@ -0,0 +1,10 @@
+RequirementMachine.pdf:
+	pdflatex RequirementMachine
+	bibtex RequirementMachine
+	pdflatex RequirementMachine
+	pdflatex RequirementMachine
+
+clean:
+	rm *.aux *.bbl *.blg *.idx *.ilg *.ind *.log *.out *.pdf *.toc
+
+.PHONY: clean

docs/RequirementMachine/RequirementMachine.bib

@@ -0,0 +1,75 @@
+@misc{se0142,
+    author    = "David Hart and Jacob Bandes-Storch and Doug Gregor",
+    title     = "{SE-0142}: Permit where clauses to constrain associated types",
+    url       = "https://github.com/apple/swift-evolution/blob/main/proposals/0142-associated-types-constraints.md",
+    year      = {2017}
+}
+@misc{se0157,
+    author    = "Doug Gregor and Erica Sadun and Austin Zheng",
+    title     = "{SE-0157}: Support recursive constraints on associated types",
+    url       = "https://github.com/apple/swift-evolution/blob/main/proposals/0157-recursive-protocol-constraints.md",
+    year      = {2017}
+}
+@misc(gensig,
+    author    = "Doug Gregor",
+    title     = "Generic Signatures",
+    url       = "https://github.com/apple/swift/blob/main/docs/ABI/GenericSignature.md",
+    year      = {2018}
+)
+@article{undecidablegroup,
+author = {Donald J. Collins},
+title = {{A simple presentation of a group with unsolvable word problem}},
+volume = {30},
+journal = {Illinois Journal of Mathematics},
+number = {2},
+publisher = {Duke University Press},
+pages = {230 -- 234},
+year = {1986},
+doi = {10.1215/ijm/1256044631},
+URL = {https://doi.org/10.1215/ijm/1256044631}
+}
+@book{andallthat, place={Cambridge}, title={Term Rewriting and All That}, DOI={10.1017/CBO9781139172752}, publisher={Cambridge University Press}, author={Baader, Franz and Nipkow, Tobias}, year={1998}}
+@Inbook{Knuth1983,
+author="Knuth, D. E.
+and Bendix, P. B.",
+editor="Siekmann, J{\"o}rg H.
+and Wrightson, Graham",
+title="Simple Word Problems in Universal Algebras",
+bookTitle="Automation of Reasoning: 2: Classical Papers on Computational Logic 1967--1970",
+year="1983",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="342--376",
+isbn="978-3-642-81955-1",
+doi="10.1007/978-3-642-81955-1_23",
+url="https://doi.org/10.1007/978-3-642-81955-1_23"
+}
+@article{SQUIER1994271,
+title = {A finiteness condition for rewriting systems},
+journal = {Theoretical Computer Science},
+volume = {131},
+number = {2},
+pages = {271-294},
+year = {1994},
+issn = {0304-3975},
+doi = {https://doi.org/10.1016/0304-3975(94)90175-9},
+url = {https://www.sciencedirect.com/science/article/pii/0304397594901759},
+author = {Craig C. Squier and Friedrich Otto and Yuji Kobayashi}
+}
+@inproceedings{guiraud:hal-00818253,
+  TITLE = {{A Homotopical Completion Procedure with Applications to Coherence of Monoids}},
+  AUTHOR = {Guiraud, Yves and Malbos, Philippe and Mimram, Samuel},
+  URL = {https://hal.inria.fr/hal-00818253},
+  BOOKTITLE = {{RTA - 24th International Conference on Rewriting Techniques and Applications - 2013}},
+  ADDRESS = {Eindhoven, Netherlands},
+  EDITOR = {Van Raamsdonk, Femke},
+  PUBLISHER = {{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}},
+  SERIES = {Leibniz International Proceedings in Informatics (LIPIcs)},
+  VOLUME = {21},
+  PAGES = {223-238},
+  YEAR = {2013},
+  MONTH = Jun,
+  DOI = {10.4230/LIPIcs.RTA.2013.223},
+  HAL_ID = {hal-00818253},
+  HAL_VERSION = {v1},
+}