WG-Traits Minutes and General Discussion

[sgrif]

forall type/region gets my vote. It most closely ties it to the actual syntax it represents in Rust. eigenvariable has a weird conflict w/ eigenclass in Ruby for me.

[mark-i-m]

So, what I am leading up to here is: what name should we adopt instead?

Matsakified

In seriousness, I think I would prefer something that lends itself nicely to being abbreviated. Also, the name should make it clear that the region is not universally qualified, which is perhaps a bit counterintuitive from a name like “forall variable”… maybe something like “dequalified variable” or “de-foralled”?

[tmandry]

Would “wildcard type” or “wildcard region” work? It ties into (I think) a familiar term for most programmers. Perhaps it doesn’t carry enough of the underlying meaning, though.

[Tom-Phinney]

IIRC, it is an abstraction of a specific item, so perhaps just prefixing the item noun (or other term) with the qualifier „abstract" would suffice.

[mark-i-m]

I feel like that is too abstract

[mark-i-m]

How about “FUIFA variables”: For Unknown Implies ForAll

[sgrif]

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

[mark-i-m]

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

[Centril]

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.

[djc]

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.

[yarrow]

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.

[gbutler]

You know that Elon Musk in his companies has forbidden the use of acronyms, right?

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.

[nikomatsakis]

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)

[rpjohnst]

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

[mark-i-m]

“forall variable”

when we remove the forall<X> binder, we get !0: Foo – that !0 is a “forall variable”

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

[nikomatsakis]

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

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.

[mark-i-m]

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

[nikomatsakis]

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…? )

[steven099]

Guinea pigs 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.

[Finn]

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.