about summary refs log tree commit diff
path: root/src/doc/rustc-dev-guide
diff options
context:
space:
mode:
authorTyler Mandry <tmandry@gmail.com>2018-11-04 09:39:31 -0600
committerTyler Mandry <tmandry@gmail.com>2018-11-04 09:50:18 -0600
commitb01cd5e3bf0034f418dd790f81967b1574fbf12f (patch)
treeea568a1b21e619e0c7da7dea65ec1f44a2abf9d6 /src/doc/rustc-dev-guide
parent6819cc84933d2cd6e20cf0763f96e3e74908d8ae (diff)
downloadrust-b01cd5e3bf0034f418dd790f81967b1574fbf12f.tar.gz
rust-b01cd5e3bf0034f418dd790f81967b1574fbf12f.zip
SLG: Replace heritage section with links to it elsewhere
Maybe we want to include this in the bibliography or something, though.
Diffstat (limited to 'src/doc/rustc-dev-guide')
-rw-r--r--src/doc/rustc-dev-guide/src/traits/slg.md57
1 files changed, 12 insertions, 45 deletions
diff --git a/src/doc/rustc-dev-guide/src/traits/slg.md b/src/doc/rustc-dev-guide/src/traits/slg.md
index d151377c55f..812afd1ec35 100644
--- a/src/doc/rustc-dev-guide/src/traits/slg.md
+++ b/src/doc/rustc-dev-guide/src/traits/slg.md
@@ -269,48 +269,15 @@ Here you can see how the forest captures both the answers we have
 created thus far *and* the strands that will let us try to produce
 more answers later on.
 
-## Heritage and acroynms
-
-This solver implements the SLG solving technique, though extended to
-accommodate hereditary harrop (HH) predicates, as well as the needs of
-lazy normalization. 
-
-Its design is kind of a fusion of [MiniKanren] and the following
-papers, which I will refer to as EWFS and NTFD respectively:
-
-> Efficient Top-Down Computation of Queries Under the Well-formed Semantics
-> (Chen, Swift, and Warren; Journal of Logic Programming '95)
-
-> A New Formulation of Tabled resolution With Delay
-> (Swift; EPIA '99)
-
-[MiniKanren]: http://minikanren.org/
-
-In addition, I incorporated extensions from the following papers,
-which I will refer to as SA and RR respectively, that describes how to
-do introduce approximation when processing subgoals and so forth:
-
-> Terminating Evaluation of Logic Programs with Finite Three-Valued Models
-> Riguzzi and Swift; ACM Transactions on Computational Logic 2013
-> (Introduces "subgoal abstraction", hence the name SA)
->
-> Radial Restraint
-> Grosof and Swift; 2013
-
-Another useful paper that gives a kind of high-level overview of
-concepts at play is the following:
-
-> XSB: Extending Prolog with Tabled Logic Programming
-> (Swift and Warren; Theory and Practice of Logic Programming '10)
-
-There are a places where I intentionally diverged from the semantics
-as described in the papers -- e.g. by more aggressively approximating
--- which I marked them with a comment DIVERGENCE. Those places may
-want to be evaluated in the future.
-
-A few other acronyms that I use:
-
-- WAM: Warren abstract machine, an efficient way to evaluate Prolog programs.
-  See <http://wambook.sourceforge.net/>.
-- HH: Hereditary harrop predicates. What Chalk deals in.
-  Popularized by Lambda Prolog.
+## See also
+
+- [chalk_solve README][readme], which contains links to papers used and
+  acronyms referenced in the code
+- This section is a lightly adapted version of the blog post [An on-demand
+  SLG solver for chalk][slg-blog]
+- [Negative Reasoning in Chalk][negative-reasoning-blog] explains the need
+  for negative reasoning, but not how the SLG solver does it
+
+[readme]: https://github.com/rust-lang-nursery/chalk/blob/239e4ae4e69b2785b5f99e0f2b41fc16b0b4e65e/chalk-engine/src/README.md
+[slg-blog]: http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/
+[negative-reasoning-blog]: http://aturon.github.io/blog/2017/04/24/negative-chalk/