WG-Traits Minutes and General Discussion

compiler traits working group
22

How about “FUIFA variables”: For Unknown Implies ForAll

23

Why is it important to make it something that is easily abbreviated?

24

Less writing. It also allows us to have a more descriptive name without worrying as much.

Moreover, what great design is complete without an acronym or abbreviation :stuck_out_tongue:

1 Like
25

My preference is for terms which you can easily search for with google so that you can find definitions and related literature. If “skolemized” accurately describes the intent or is close enough, then that should be kept, if not, it shouldn’t be and we should pick something more accurate in the PLT literature.

3 Likes
26

You know that Elon Musk in his companies has forbidden the use of acronyms, right? They make your language actively harder to penetrate for anyone new coming up to speed on your jargon.

27

It looks like mathematicians use “Skolemization” for the process of removing existential quantifiers by a process that introduces constant and function symbols, and Herbrandization for the dual process of removing universal quantifiers. But folks working in automated theorem proving seem to use skolemization in the broadened sense of removing quantifiers, both universal and existential.

So the usage is correct in this context. On the other hand, a google search for “skolemized” is much more likely to bring up the mathematical sense of Skolemization than the theorem-proving sense.

The only thing that comes to my mind as a replacement for “skolemized” is “de-quantified” type or region, but I think that’s even more confusing.

1 Like
28

Good thing we have Elon to tell us the right way to do things. I'm sure that all the organizations that regularly use acronyms CORRECTLY (important point) can't wait to get rid of them.

Correct use of acronyms are to use the full, expanded version at the first use in a communication followed by the acronym in parenthesis. Then, in the remainder of the communication, just use the acronym. If the communication is long (like a book with several chapters), you should use the full, expanded version at the first use in each chapter. A couple of page essay, memo, tutorial, or press-release would be correct to only use the full, expanded version at the first use in the document.

If those rules are followed, acronyms ABSOLUTELY facilitate clear, concise communication.

29

I think I like the following terms best:

  • “bound variable”
    • the (second) X in forall<X> { X: Foo }
      • that is, a reference back to a binder that has not been “removed” from the term
  • “forall variable”
    • when we remove the forall<X> binder, we get !0: Foo – that !0 is a “forall variable”
  • “exists variable”
    • an inference variable, which arises from removing a exists<X> { ... } binder in a goal (or instantiating a forall<X> binder in a clause)
2 Likes
30

@gbutler- could you please use a little less snark and all-caps here (and in general)? It’s enough to make your point well once and let others make theirs.

1 Like
31

I still find this a bit counterintuitive. A forall variable is one where we removed (skolemized) the forall...

1 Like
32

Perhaps; I think the implicit thing is that it is a "free" forall variable - i.e., the binder has moved "out" of the term, and this is telling you what sort of binder it was.

33

I guess that’s fair. I don’t have really strong feelings… I just feel like the name should communicate a bit more about why we are skolemizing: if we can prove that something is true for an arbitrary unknown X, then we can prove it forall<X>… When I was reading your PR in the rustc-guide about skolemization, the paragraph where you explained that is where everything clicked for me :slight_smile:

34

One good thing about the term “skolemize” is that it is quite unique, making it easy to look up the definition. “forall” doesn’t seem to share this property. Perhaps there is another term that can capture this intuition and be sort of unique. “Universal stand-in”? “Representative”? “Exemplar”? “Specimen”? (Can you tell I’m looking at a thesaurus…? :slight_smile:)

35

Guinea pigs :wink: Or token/surrogate values. Calling them “variables” seems like it would be misleading, since what the process does is replace universally quantified variables with arbitrary constants.

36

If you actually want to understand skolemization, I recommend at first you read the first section of this lecture:

Lecture 9: Analytic Tableaux vs. Refinement logic. In: CS 4860: Applied Logic (Fall 2012), Cornell University: Computer Science.

Now, note that Fφ is a shorthand for I(φ)=false, where I is an interpretation. An interpretation is simply a row of the truth table: each variable gets a truth value. One does the following:

(1)  (|= φ) ⇔ ∀I(I(φ)=true) ⇔ ¬∃I(I(φ)=false)

and shows by analytic tableaux method that I(φ)=false is not satisfiable. Note that (1) is a statement in metalanguage, i.e. the quantifiers in (1) do not belong to object language. By ∀I and ∃I you basically express a quantification over all rows of the truth table.

By the way: try to compare analytic tableaux complexity with brute force truth table evaluation.

Next, the question arises, whether it is possible to transfer this method from propositional calculus to first-order predicate calculus. It must be said that predicate calculus is more complex:

  • you need to introduce the notion of free/bound variables,
  • interpretations can also assign functions to function symbols,
  • the number of interpretations may be infinite.

Some analytic tableaux examples are stated in Wikipedia: First-order logic tableau.

By skolemization you obtain an equisatisfiable formula with existential quantifiers removed. I believe an existential quantifier would mean a tableaux node with an infinite number of edges, and by skolemization you shrink them together to a single edge. The formula will not be equivalent, but this is not a problem, as we only need to show satisfiability/unsatisfiability.

1 Like
37

“Skolemized” is probably the Rust compiler jargon that has befuddled me the most and for the longest time. In fact it wasn’t until someone in this thread spelled out that some folks use “skolemization” for eliminating all quantifiers that it finally clicked for me. And this is despite, or perhaps because, I learned of skolem normal form (and herbrand normal form, the dual for eliminating universal quantifiers) in mathematical logic before I ever got in contact with Rust. But for what it’s worth, this semester I took a lecture on automated theorem proving and even there I didn’t encounter skolemization as a thing you do to universal quantifiers as well (only for existential ones). With that background, I hope it’s understandable that I hold a bit of a grudge against the term and would like to see it replaced.

On the other hand, I believe if this had been properly spelled out somewhere (say, the rustc guide), I probably would have found it or be referred to it early on in my confusion and everything would have been well. The obscurity of the term is probably an advantage from this perspective for the majority of people who haven’t had a mathematical logic lecture before coming to Rust — many people haven’t heard of it and can’t make head nor tail of it, so they immediately go look it up. Then again, googling the term will likely result in misleading results, you’d have to search the rustc guide or a very narrow range of research literature.

So in summary I think “skolem” is probably fine, as long as it’s excessively documented in every available location what that means (but this is important regardless of what term is picked).

3 Likes
38

I am reminded of a conversation that @scalexm and I were having. We were discussing how to represent types and things, and the differences between rustc and chalk. It occurs to me that we might avoid the question if we adopted the “univariant” scheme I describe below, in which case everything is just a “variable” – but having written that out, I think the downsides are large enough it’s probably best to be avoided for now.

In Rustc, right now we have three distinct region variants, all of which might conceptually be considered variables:

  • ReLateBound – bound within some enclosing type or term
    • e.g., the 'x in for<'x> T: Trait<'x> or for<'x> fn(&'x u32)
    • of course if you are iterating over terms you might encounter it, particularly when you “skip” through a Binder<T> type to the T within
  • ReSkolemized – a universally quantified thing bound in the “environment”, essentially (inference context, more specifically)
    • this is used when doing the ‘leak check’, but is also the subject of discussion
  • ReVar – an existentially quantified thing bound in the environment (again, inference context, more specifically)

In Chalk, we also have some distinctions, but fewer. We represent the equivalent of ReVar and ReLateBound using the same variant – “variable”, but we use debruijn indices to track the difference. That is, if you have an inference variable with index 0, then when you enter a for<'x> binder, it would be referenced with index 1:

T: Foo<'?0, for<'x> fn(&'?0 u32, &'?1 u32)>
       ^^^                        ^^^
       these are both references to inference variable zero

In Chalk, we still distinguish the “universal” case, which we represent as a kind of !1 where 1 is a universe index, but one could imagine not doing that. Instead, we could represent everything with just a debruijn index. When that debruijn index exceeds the binders in the term, it refers into the surrounding inference context, and that context would track whether it was universally bound (“skolemized”) or existentially bound (“inference variable”).

I find this appealingly simple. It has some efficiency gains (perhaps minor):

Notably, if you have a fully canonicalized term, it is essentially a “mini inference context”. We can create an inference context around it without doing any substitution of any kind (chalk is also able to do this).

But I also see some concrete downsides:

First off, you wouldn’t be able to use match and a variant to determine which of the three cases you are dealing with; you’d just get an index and you’d have to go look into the inference context to figure it out.

Second, right now we keep “things that refer into the inference context” interned and allocated in a separate memory arena, and we use the variants to figure out where things belong. The scheme breaks down if ?0 is “sometimes” bound within a global term and sometimes the surrounding infcx.

39

Yeah I was wondering about this. Here are some more possible terms:

  • Dummy
  • Archetype / ArchetypalType / ArchetypalRegion

Looking through synonyms of "representative", I am intrigued by "archetype". It has sort of kind of the right meaning:

the original pattern or model of which all things of the same type are representations or copies

It is not in widespread use within computing that I know of, so it's kind of unique and easily referenced.

Alternatively, the synonyms for dummy are interesting:

  • ersatz
  • artificial
  • mimic
  • mock

Artificial sounds kind of nice?

40

OK, having thought a lot about it, I now learn towards Placeholder as the term of choice. It’s kind of distinctive, but also everyday, and it means exactly what it says:

“When you encounter a forall<T> { G } goal, we don’t know yet what T will be. So we substitute in a special “placeholder” type (written like !1) for T, and try to prove that G holds using that.”

TyPlaceholder etc feels good.

8 Likes
41

Had our next planning meeting. There’s been some good activity – check the minutes for details. Here are the upcoming things we’re focusing on for this week: