Add glossary #51

fabric-and-ink · 2017-06-21T03:34:40Z

This a draft for a glossary for this crate (see #41). I chose terms that I found inside the crate and added some that seemed appropriate.

Now I need feedback, @nikomatsakis, @aturon, @withoutboats :)

Which terms are unnecessary? Which terms are still missing from the list? Which terms need more explanation?
Some terms are still lacking an description. These are the ones that I would have to guess.
Please point out all factual & grammatical errors and wording improvements.
More pointers to literature :)

Rendered

fabric-and-ink · 2017-06-21T03:41:24Z

GLOSSARY.md

+| 0111        | ||              | Disjunction; or                  |
+| 1001        | <=>             | Equivalence; if and only if; iff |
+| 1101        | =>              | Implication; if ... then         |
+```


This table could not be rendered correctly in markdown because of the || operator and I didn't like the workaround :(

Since the || operator is not used at all in Chalk, maybe you could just drop it? I think that would avoid some confusion. Or maybe you just want to be exhaustive in a general way and then that's fine.

Generality is not my goal, so I will drop it.

fabric-and-ink · 2017-06-21T03:42:07Z

GLOSSARY.md

+  `a` is a free variable.
+- A sum `\sum_n x_n` binds the index variable `n`.
+
+## Canonical


"(empty)" missing...

Maybe somebody can explain this term?

So Canonical applies to an object which contains variables (e.g., a goal) and means that:

we have replaced some variables with their value if any (i.e. we have applied our current "knowledge")

we have rebound De Bruijn indices to lower ones

Chalk only deals with goals in canonical form.

For example, when dealing with a goal like: forall<0,1> { 0: Foo && 1: Bar }. Here we have two different indices because there are two different variables, and this goal is in canonical form.

In order to process it we will process each subgoal (namely 0: Foo and 1: Bar) separately, and so when we process 1: Bar, this goal is not in canonical form because it could be written as 0: Bar (lower De Bruijn indices). So we canonicalize this subgoal, process it, and then feed back the answer to the top level goal.

scalexm · 2017-06-21T07:49:36Z

GLOSSARY.md

+
+## DeBrujin Index
+(empty)
+


Once you have filled this section, you may want to move the Canonical section just after this one, since in particular Canonical deals with rebounding variables to lower DeBruijn indices.

I would like to keep the terms in alphabetical order. Can you explain both terms and how they interact?

Oh right it's a glossary!
So I'll start with De Bruijn indices anyway. When you have a formula: forall<T> { exists<U> { T: Foo<Item = U> } }, you don't want to deal with variable names like T and U because these are difficult to handle. So De Bruijn indices transform each variable name into a natural number, for example the previous query would be transformed in forall<0> { exists<1> { 0: Foo<Item = 1> } }.

Ok, then these indices aren't really more complicated than what I have read. I wasn't sure if there was some small, magical detail that I was missing :)

Reading the code I noticed that these indices seem to have a close relationship to the UniverseIndex (not sure about the exact name right now). What is an Universe and how is it related to our formulas?

Sorry I missed this one! So UniverseIndex indicates the number of universall quantifiers we are within. Examples:

i32: Foo // in universe 0 here

forall<T> { // in universe 1 here exists<U> { forall<V> { // in universe 2 here ... } } }

When we canonicalize, we just recall the universe indices of the re-bound variables.

scalexm · 2017-06-21T07:50:57Z

GLOSSARY.md

+## Datum
+(empty)
+
+## DeBrujin Index


Nit: Debruijn :)

Ah... yes :)

scalexm · 2017-06-21T07:52:49Z

GLOSSARY.md

+
+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.
+


Maybe you should explain how Horn clauses relate to Chalk and logic programming in general (ie they can be understood as A <= B && C && D ... && Z where A, ..., Z are literals)

This is an important point that I didn't really grasp. Could you elaborate a bit?

In propositional calculus, a Horn clause is a clause of the form A || !B || ... || !Z with at most one positive literal (denoted A here). Taking the implication P => Q as a shortcut for !P || Q, we can rewrite the clause above like B && C && ... && Z => A.

So in logic programming, a Horn clause is understood as this latter form, ie exactly one consequence following from a certain number of conditions. Every logical rule that Chalk knows is of this form, and it will only use this kind of rules in order to give a result to a goal.

More questions came up.

To me Horn clauses seem to be of a "weaker" form than Definite clauses, at least with respect to the logical equivalence B && C && ... => A. In the case of Horn clauses it is possible that there is no A as a consequence of B && C && .... How is this possibility treated in chalk? I such a case rejected?

You mentioned rules in your last sentence. Could you explain what these rules are exactly and give some examples?

Thanks!

Sorry, I should have been more explicit indeed! So in Chalk we don't really deal with Horn clauses without a consequence (called negative Horn Clauses). Well in some sense goals can be seen as such clauses, but that's it.

By rules, I meant the clauses that Chalk infers from a (pseudo) Rust program and definitely holds for true. For example, given the following program:

struct MyStruct<T> { } impl<T> Foo for MyStruct<T> where T: Clone, T: Bar { }

Chalk will infer something like this (in form of a Horn clause):
(T: Clone) && (T: Bar) => (MyStruct<T>: Foo)
which in logic programming is traditionally denoted as:
(MyStruct<T>: Foo) :- (T: Clone), (T: Bar)
i.e. "consequence IF(:-) condition1, conditon2, ..."

You'll note that since there is a type parameter T, the latter clause should hold for every type T. So that means that in fact we do not have one clause here, but an infinite family of them (one for each possible value of T).

Also note that there can be no conditions at all, like in:

struct MyStruct { } impl Foo for MyStruct { }

which will be lowered into (MyStruct: Foo)., i.e. this is a ground fact that Chalk holds for true.

I see! Thank you for the explanation.

scalexm · 2017-06-21T07:53:50Z

GLOSSARY.md

+## Goal
+With a set of given types, traits and impls, a goal specifies a problem where
+types need to be found that satisfy the problem.
+


Maybe add an example of such a goal?

scalexm · 2017-06-21T07:55:05Z

GLOSSARY.md

+
+## Projection
+Projection is the reference to a field or (in the context of Rust) to a type.
+


You might want to give an example of what we call a projection in Chalk.

Will do. I think the Iterator/Item case should be a good example, right?

Yes indeed :)

I'm a bit unsure about Projection... I understand what Normalization is and added an example accordingly. Can you provide an example for this one?

So these two are related. A projection is a reference to an associated type, like <T as Iterator>::Item. Normalization is the process of telling what this associated type is (specifying the projection), which is denoted in Chalk by <T as Iterator>::Item ==> i32 for example

scalexm · 2017-06-21T07:56:49Z

GLOSSARY.md

+Unification is the process of solving a formula. That means unification finds
+values for all the free variables of the formula that satisfy it. In the context
+of chalk the values refer to types.
+


An example here would be valuable :)

scalexm · 2017-06-21T08:00:24Z

GLOSSARY.md

+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)`.
+


You should add that in the context of Chalk, we actually ask for something stronger than "at least one": we want that there exists exactly one since we are trying to determine what type the user intended. If we have more than one possible values, we consider the result as ambiguous.

Ah, this is important :) and did not really know that. I will add this information.

fabric-and-ink · 2017-07-02T17:54:59Z

The following descriptions are still missing/incomplete (and I need help with them because I have only a vague or no clue :) )

Datum
Universe
Well-formed
Projection

By the way: how do I provide a link to the rendered version of the text? I have seen it before but I don't know how to do it.

lqd · 2017-07-02T20:56:55Z

@fabric-and-ink you mean a link to your branch's glossary.md like this ? Rendered

fabric-and-ink · 2017-07-03T13:42:12Z

Exactly, thanks!

nikomatsakis · 2017-07-07T14:56:54Z

Datum

This is just the singular of "data". It is used to indicate the "data" about an impl or trait, as I recall, in the IR, but has no particular meaning other than being relatively distinctive. In general, I think we're phasing most of those "datums" out anyway, since they were basically used to "cheat" in the trait handling, by looking at the original source program rather than the pure lowered form.

Universe

When you are type-checking something like fn foo<A>(x: A) { ... }, we say that the name A is in a different "universe" from the structs. This is because it is a name that is only valid inside the body of foo, and it can never be named from outside foo. Hence "universe" refers to kind of "the set of things you can talk about at a particular point". Universes are arranged into a tree: things in the root universe can be named from anywhere, because if you are in universe X, you can name all the things in X or any ancestor of X, but not the other universes.

Well-formed

The "well-formed" conditions are basic conditions that are needed to ensure that some request is valid. So, for example, if I have struct HashSet<T: Hash>, then HashSet<i32> is well-formed because i32: Hash. But something like HashSet<NotHash>, where NotHash is a type that does not implement Hash, would not be well-formed. Similarly, if you have trait Foo<T: Hash>, then Bar: Foo<i32> is well-formed (written WF(Bar: Foo<i32>)), because i32: Hash, but Bar: Foo<NotHash> would not be. Note that just because Bar: Foo<i32> is well-formed doesn't mean that it is true -- it basically means that the conditions are correct such that Bar: Foo<i32> could be implemented, but not that it necessarily is.

As a more concrete example, in the Rust stdlib we have trait Eq: PartialEq, which is short for trait Eq where Self: PartialEq. This implies that if you have impl Eq for Foo, you must also have impl PartialEq for Foo. We say then that WF(Foo: Eq) holds if Foo: PartialEq -- that is, those are the conditions in which one is allowed to implement Eq for Foo, even if you do not actually do so.

Projection

A "projection" is a general term meaning to extract some "part" of something. In the case of chalk, it mostly refers to associated types. So when you have <T as Iterator>::Item, this is "projecting" Item "out of" T as Iterator. That is, it is determining what value is given for Item in the impl of Iterator for T.

nikomatsakis · 2017-07-07T14:58:18Z

GLOSSARY.md

+in an unambiguous way in order to work with numbers instead of the names of the
+literals. Given the example `forall<T> { exists<U> { T: Foo<Item=U> } }` the
+literal names `U` and `T` are replaced with `0` and `1` respectively: `forall<0>
+{ exists<1> { 0: Foo<Item=1> } }`.


Maybe: "More generally, the debruijn index is the index of the binder where a name was defined, starting from the innermost binder and working out."

nikomatsakis · 2017-07-07T15:00:59Z

GLOSSARY.md

+## 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.


I think we could make this a bit more intuitive. I would given an example like this:

To get an intuition for skolemization, consider this Rust function:

fn foo<T: Hash>() { ... }

When we type-check the body of foo(), we don't know yet what the type T will be. So we introduce a "skolemized" type -- meaning, basically, a fresh type that is distinct from all other types in the program. The only thing we know about this skolemized type T is that it implements Hash. Therefore, if we can successfully type-check the function, we know that it should type-check with any other type, so long as that type implements Hash (for this to work, we have to ensure that knowing more about a type never interferes with type-checking).

Skolemization also occurs in other contexts. For example, if you have a "higher-ranked" type like for<'x> fn(&'x u32) -> &'x u32, then 'x is a bound lifetime that will be instantiated each time the function is called. We may however want to check something about the function type in the abstract, without knowing exactly what 'x is. In that context, we could skolemize 'x and check the contents that way.

Thank you for your thorough explanations! I will work them in during the next days :)

A glossary is a great idea btw

nikomatsakis · 2017-07-17T12:32:37Z

@fabric-and-ink do you mean rebasing? I'm reluctant to merge with merge commits in the PR itself.

fabric-and-ink · 2017-07-17T20:16:52Z

Sorry! Made a mistake... I want to squash everything when this PR is ready.

fabric-and-ink · 2017-07-26T11:05:24Z

(Still working on it :) )
(PS: I ordered more literature. A few things still confuse me 🙂 )

nikomatsakis · 2017-10-09T13:05:29Z

@fabric-and-ink is there any reason not to merge this? seems like good stuff so far! :)

fabric-and-ink · 2017-10-10T10:53:52Z

Glad to hear! I think for a first iteration it is almost finished. There are still some descriptions missing or without an example. I will add them in a few days.

fabric-and-ink · 2017-10-10T14:34:37Z

Ok, I think this should be good for now.

nikomatsakis · 2017-10-10T18:21:37Z

🚀 thanks @fabric-and-ink !

fabric-and-ink commented Jun 21, 2017

View reviewed changes

fabric-and-ink mentioned this pull request Jun 21, 2017

Improve documentation #41

Closed

1 task

fabric-and-ink changed the title ~~[WIP] Add first draft of glossary~~ [WIP] Add glossary Jun 21, 2017

scalexm reviewed Jun 21, 2017

View reviewed changes

fabric-and-ink mentioned this pull request Jul 4, 2017

refactor occurs check into a folder #25

Closed

nikomatsakis reviewed Jul 7, 2017

View reviewed changes

Add a glossary

e2824a1

fabric-and-ink changed the title ~~[WIP] Add glossary~~ Add glossary Oct 10, 2017

Add glossary reference to README.md

dcbf6f1

nikomatsakis merged commit c702e6b into rust-lang:master Oct 10, 2017


		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.


		## Projection
		Projection is the reference to a field or (in the context of Rust) to a type.

Add glossary #51

Add glossary #51

Conversation

fabric-and-ink commented Jun 21, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fabric-and-ink Jun 21, 2017 • edited Loading

Choose a reason for hiding this comment

fabric-and-ink Jun 21, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fabric-and-ink Jul 5, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fabric-and-ink commented Jul 2, 2017 • edited Loading

lqd commented Jul 2, 2017

fabric-and-ink commented Jul 3, 2017

nikomatsakis commented Jul 7, 2017

Choose a reason for hiding this comment

nikomatsakis Jul 7, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikomatsakis commented Jul 17, 2017

fabric-and-ink commented Jul 17, 2017

fabric-and-ink commented Jul 26, 2017 • edited Loading

nikomatsakis commented Oct 9, 2017

fabric-and-ink commented Oct 10, 2017

fabric-and-ink commented Oct 10, 2017

nikomatsakis commented Oct 10, 2017

fabric-and-ink commented Jun 21, 2017 •

edited

Loading

fabric-and-ink Jun 21, 2017 •

edited

Loading

fabric-and-ink Jun 21, 2017 •

edited

Loading

fabric-and-ink Jul 5, 2017 •

edited

Loading

fabric-and-ink commented Jul 2, 2017 •

edited

Loading

nikomatsakis Jul 7, 2017 •

edited

Loading

fabric-and-ink commented Jul 26, 2017 •

edited

Loading