Merge pull request #405 from crlf0710/book-and-readme

Copy chalk related content from rustc-dev-guide to chalk-book.

Author: detrumi

GLOSSARY.md

@@ -1,203 +1,3 @@
 # Glossary
-This is a glossary of terminology (possibly) used in the chalk crate.
 
-## Binary connective
-There are sixteen logical connectives on two boolean variables. The most
-interesting in this context are listed below. There is also a truth table given
-which encodes the possible results of the operations like this
-
-```
-f(false, false) f(false, true) f(true, false) f(true, true).
-```
-
-As a shorthand the resulting truth table is encoded with `true = 1` and `false =
-0`.
-
-| Truth table | Operator symbol | Common name                      |
-|-------------|-----------------|----------------------------------|
-| 0001        | &&              | Conjunction; and                 |
-| 1001        | <=>             | Equivalence; if and only if; iff |
-| 1101        | =>              | Implication; if ... then         |
-
-## Binder
-A binder is an expression that binds a literal to a certain expression.
-Examples for binders:
-
-- The universal quantifier `forall(a)` states that a certain condition holds for
-  all allowed values for `a`.
-- A function definition `f(x) = a * x` is a binder for the variable `x` whereas
-  `a` is a free variable.
-- A sum `\sum_n x_n` binds the index variable `n`.
-
-## Canonical Form
-A formula in canonical form has the property that its DeBruijn indices are
-minimized. For example when the formula `forall<0, 1> { 0: A && 1: B }` is
-processed, both "branches" `0: A` and `1: B` are processed individually. The
-first branch would be in canonical form, the second branch not since the
-occurring DeBruijn index `1` could be replaced with `0`.
-
-## Clause
-In the A clause is the disjunction of several expressions. For example the clause
-`condition_1 || condition_2 || ...` states that at least one of the conditions
-holds.
-
-There are two notable special cases of clauses. A *Horn clause* has at most one
-positive literal. A *Definite clause* has exactly one positive literal.
-
-*Horn clauses* can be written in the form `A || !B || !C || ...` with `A` being
-the optional positive literal. Due to the equivalence `(P => Q) <=> (!P || Q)`
-the clause can be expressed as `B && C && ... => A` which means that A is true
-if `B`, `C`, etc. are all true. All rules in chalk are in this form. For example
-
-```
-struct A<T> {}
-impl<T> B for A<T> where T: C + D {}
-```
-
-is expressed as the *Horn clause* `(T: C) && (T: D) => (A<T>: B)`. This formula
-has to hold for all values of `T`. The second example
-
-```
-struct A {}
-impl B for A {}
-impl C for A {}
-```
-
-is expressed as the *Horn clause* `(A: B) && (A: C)`. Note the missing
-consequence.
-
-## DeBruijn Index
-DeBruijn indices numerate literals that are bound in an unambiguous way. The
-literal is given the number of its binder. The indices start at zero from the
-innermost binder increasing from the inside out.
-
-Given the example `forall<T> { exists<U> { T: Foo<Item=U> } }` the
-literal names `U` and `T` are replaced with `0` and `1` respectively and the names are erased from the binders: `forall<_>
-{ exists<_> { 1: Foo<Item=0> } }`.
-
-## Formula
-A formula is a logical expression consisting of literals and constants connected
-by logical operators.
-
-## Goal
-With a set of type variables, given types, traits and impls, a goal specifies a
-problem which is solved by finding types for the type variables that satisfy the
-formula. For example the goal `exists<T> { T: u32 }` can be solved with `T =
-u32`.
-
-## Literal
-A literal is an atomic element of a formula together with the constants `true`
-and `false`. It is equivalent to a variable in an algebraic expressions. Note
-that literals are *not* the same as the type variables used in specifying a
-goal.
-
-## Normal form
-To say that a statement is in a certain *normal form* means that the pattern in
-which the subformulas are arranged fulfil certain rules. The individual patterns
-have different advantages for their manipulation.
-
-### Conjunctive normal form (CNF)
-A formula in CNF is a conjunction of disjunctions. For example `(x1 || x2 ||
-x3) && (x4 || x5 || x6)` is in CNF.
-
-### Disjunctive normal form (DNF)
-A formula in DNF is a disjunction of conjunctions. For example `(x1 && x2 &&
-x3) || (x4 && x5 && x6)` is in DNF.
-
-### Negation normal form (NNF)
-A formula in NNF consists only of literals, the connectives `&&` and `||` and
-`true` and `false`.
-
-### Prenex normal form (PNF)
-All quantifiers are on the highest level of a formula and do not occur inside
-the subformulas of the expression.
-
-- `forall(x). exists(y). forall(z). P(x) && P(y) => P(z)` is in PNF.
-- `(exists(x). P(x)) => exists(y). P(y) && forall(z). P(z)` is *not* in PNF.
-
-## Normalization
-Normalization is the process of converting an associated type to a concrete
-type. In the case of an iterator this would mean that the associated `Item` type
-is replaced with something more meaningful with respect to the individual
-context (e.g. `u32`).
-
-## Projection
-Projection is the reference to a field or (in the context of Rust) to a type
-from another type.
-
-## Satisfiability
-A formula is satisfiable iff there is a valuation for the atoms inside the
-formula that makes it true.
-
-## Unification
-Unification is the process of solving a formula. That means unification finds
-values for all the free literals of the formula that satisfy it. In the context
-of chalk the values refer to types.
-
-## Universe
-A universe sets the scope in which a particular variable name is bound. (See
-*Binder*.) A universe can encapsulate other universes. A universe can
-be contained by only one parent universe. Universes have therefore a tree-like
-structure. A universe can access the variable names of itself and the parent
-universes but not of the sibling universes.
-
-## Well-formed
-A formula is well-formed if it is constructed according to a predefined set of
-syntactic rules.
-
-In the context of the Rust type system this means that basic rules for type
-construction have to be met. Two examples: 1) Given a struct definition
-
-```rust
-struct HashSet<T: Hash>
-```
-then a type `HashSet<i32>` is well-formed since `i32` implements `Hash`. A type
-`HashSet<NoHash>` with a type `NoHash` that does not implement the `Hash` trait
-is not well-formed.
-
-2) If a trait demands by its definition the implementation of further traits
-for a certain type then these secondary traits have to be implemented as well.
-If a type `Foo` implements `trait Eq: PartialEq` then this type has to implement
-`trait PartialEq` as well. If it does not, then the type `Foo: Eq` is not well
-formed according to Rust type building rules.
-
-## Quantifier
-
-### Existential quantifier
-A formula with the existential quantifier `exists(x). P(x)` is satisfiable if
-and only if there exists at least one value for all possible values of x which
-satisfies the subformula `P(x)`.
-
-In the context of chalk, the existential quantifier usually demands the
-existence of exactly one instance (i.e. type) that satisfies the formula (i.e.
-type constraints). More than one instance means that the result is ambiguous.
-
-### Universal quantifier
-A formula with the universal quantifier `forall(x). P(x)` is satisfiable
-if and only if the subformula `P(x)` is true for all possible values for x.
-
-### Helpful equivalences
-- `not(forall(x). P(x)) <=> exists(x). not(P(x))`
-- `not(exists(x). P(x)) <=> forall(x). not(P(x))`
-
-## Skolemization
-Skolemization is a technique of transferring a logical formula with existential
-quantifiers to a statement without them. The resulting statement is in general
-not equivalent to the original statement but equisatisfiable.
-
-## Validity
-An argument (*premise* therefore *conclusion*) is valid iff there is no
-valuation which makes the premise true and the conclusion false.
-
-Valid: `A && B therefore A || B`. Invalid: `A || B therefore A && B` because the
-valuation `A = true, B = false` makes the premise true and the conclusion false.
-
-## Valuation
-A valuation is an assignment of values to all variables inside a logical
-formula.
-
-# Literature
-- Offline
-    - "Introduction to Formal Logic", Peter Smith
-    - "Handbook of Practical Logic and Automated Reasoning", John Harrison
-    - "Types and Programming Languages", Benjamin C. Pierce
+Please see [Appendix A: Glossary and terminology](`http://rust-lang.github.io/chalk/book/glossary.html`) in Chalk book.

README.md

@@ -1,4 +1,6 @@
 [![Build Status](https://github.com/rust-lang/chalk/workflows/CI/badge.svg)](https://github.com/rust-lang/chalk/actions?workflow=CI)
+[![Chalk Book](https://img.shields.io/badge/book-chalk-blue.svg)](https://rust-lang.github.io/chalk/book/)
+[![Rust Documentation](https://img.shields.io/badge/api-rustdoc-blue.svg)](https://rust-lang.github.io/chalk/chalk/)
 
 # chalk
 

book/src/SUMMARY.md

@@ -14,9 +14,21 @@
         - [Fold and the Folder trait](./types/operations/fold.md)
 - [Representing traits, impls, and other parts of Rust programs](./rust_ir.md)
 - [Lowering Rust IR to logic](./clauses.md)
-    - [Unification and type equality](./clauses/type_equality.md)
+    - [Goals and clauses](./clauses/goals_and_clauses.md)
+    - [Type equality and unification](./clauses/type_equality.md)
+    - [Implied bounds](./clauses/implied_bounds.md)
+    - [Lowering rules](./clauses/lowering_rules.md)
+    - [Well-formedness checking](./clauses/wf.md)
+- [Canonical queries](./canonical_queries.md)
+    - [Canonicalization](./canonical_queries/canonicalization.md)
 - [How does the engine work](./engine.md)
     - [Major concepts](./engine/major_concepts.md)
     - [Logic](./engine/logic.md)
         - [Coinduction](./engine/logic/coinduction.md)
-- [Glossary and terminology](./glossary.md)
+    - [SLG Solver](./engine/slg.md)
+
+---
+
+[Appendix A: Glossary and terminology](./glossary.md)
+[Appendix B: Bibliography](./bibliography.md)
+[Appendix C: Incomplete chapters](./todo.md)

book/src/bibliography.md

@@ -0,0 +1,45 @@
+# Bibliography
+
+If you'd like to read more background material, here are some
+recommended texts and papers:
+
+## Blog Posts
+
+* [Lowering Rust traits to logic](http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/)
+* [Unification in Chalk, part 1](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/)
+* [Unification in Chalk, part 2](http://smallcultfollowing.com/babysteps/blog/2017/04/23/unification-in-chalk-part-2/)
+* [Negative reasoning in Chalk](https://aturon.github.io/blog/2017/04/24/negative-chalk/)
+* [Query structure in chalk](http://smallcultfollowing.com/babysteps/blog/2017/05/25/query-structure-in-chalk/)
+* [Cyclic queries in chalk](http://smallcultfollowing.com/babysteps/blog/2017/09/12/tabling-handling-cyclic-queries-in-chalk/)
+* [An on-demand SLG solver for chalk](http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/)
+
+## Papers
+
+<a name="pphhf"></a>
+
+["A proof procedure for the logic of Hereditary Harrop formulas"][pphhf],
+by Gopalan Nadathur. This paper covers the basics of universes,
+environments, and Lambda Prolog-style proof search. Quite readable.
+
+[pphhf]: https://dl.acm.org/citation.cfm?id=868380
+
+<a name="slg"></a> 
+
+["A new formulation of tabled resolution with delay"][nftrd], by
+Theresa Swift. This paper gives a kind of abstract treatment of the
+SLG formulation that is the basis for our on-demand solver.
+
+[nftrd]: https://dl.acm.org/citation.cfm?id=651202
+
+
+## Books
+* "Introduction to Formal Logic", Peter Smith
+* "Handbook of Practical Logic and Automated Reasoning", John Harrison
+* "Types and Programming Languages", Benjamin C. Pierce
+* [Programming with Higher-order Logic][phl], by Dale Miller and Gopalan
+Nadathur, covers the key concepts of Lambda prolog. Although it's a
+slim little volume, it's the kind of book where you learn something
+new every time you open it.
+
+[phl]: https://www.amazon.com/Programming-Higher-Order-Logic-Dale-Miller/dp/052187940X
+