Skip to content

Commit

Permalink
Copy most contents from rustc-dev-guide.
Browse files Browse the repository at this point in the history 
regions.md and lowering-module.md was excluded.
  • Loading branch information
@crlf0710
crlf0710 committed Apr 19, 2020
1 parent 00ebd83 commit 1717735
Show file tree
Hide file tree
Showing 17 changed files with 3,323 additions and 205 deletions.
202 changes: 1 addition & 201 deletions GLOSSARY.md
View file
Original file line number Diff line number Diff line change
@@ -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.
16 changes: 14 additions & 2 deletions book/src/SUMMARY.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
45 changes: 45 additions & 0 deletions book/src/bibliography.md
View file
Original file line number Diff line number Diff line change
@@ -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

Loading

0 comments on commit 1717735

Please sign in to comment.