diff options
| author | Tyler Mandry <tmandry@gmail.com> | 2018-11-04 09:39:31 -0600 |
|---|---|---|
| committer | Tyler Mandry <tmandry@gmail.com> | 2018-11-04 09:50:18 -0600 |
| commit | b01cd5e3bf0034f418dd790f81967b1574fbf12f (patch) | |
| tree | ea568a1b21e619e0c7da7dea65ec1f44a2abf9d6 /src/doc/rustc-dev-guide | |
| parent | 6819cc84933d2cd6e20cf0763f96e3e74908d8ae (diff) | |
| download | rust-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.md | 57 |
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/ |
