Glossary and terminology

This is a glossary of terminology (possibly) used in the chalk crate.

Notation

Basic notation

Rules

• forall<T> { (Vec<T>: Clone) :- (T: Clone): for every T, Vec<T> implements Clone if T implements Clone

Queries

• Vec<i32>: Clone: does Vec<i32> implement Clone?
• exists<T> { Vec<T>: Clone }: does there exist a T such that Vec<T> implements Clone?

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.

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 De Bruijn 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 De Bruijn index 1 could be replaced with 0.

Clause

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.

De Bruijn Index

De Bruijn 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> } }.

As another example, in forall<X, Y> { forall <Z> { X } }, X is represented as ^1.0. The 1 represents the De Bruijn index of the variable and the 0 represents the index in that scope: X is bound in the second scope counting from where it is referenced, and it is the first variable bound in that scope.

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 fulfill 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

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.

Fixed-Points

A fixed-point of a function f is a value x for which f(x)=x. Similarly a pre-fixed-point is defined as x ≤ f(x), whereas for a post-fixed-point it holds that f(x) ≤ x.

A least fixed-point (lfp) of f is the fixed-point x of f for which all other fixed-points y are greater or equal (i.e. if f(y)=y then x ≤ y). Similarly, a greatest fixed-point (gfp) is greater or equal than all other fixed-points. If f is a function on sets, the least fixed-point is defined as the intersection of all pre-fixed-points, which are then defined as sets x for which x ⊆ f(x). The greatest fixed-point is in this case the union of all post-fixed-points, respectively.

This simple definition of lfp and gfp can also be lifted to general lattices. The results for Chalk goals form such a lattice and, thus, every solver for such goals tries to find such fixed-points.