[TYPES] Re: terminology for different kinds of proof terms?
Joe Wells
jbw at macs.hw.ac.uk
Thu Jan 27 14:31:09 EST 2005
A few days ago, I asked this:
> I am seeking pointers to definitions of terminology for different
> kinds of proof terms.
>
> At the most basic level, I understand the phrase "proof term" to refer
> to syntactic objects that are added to the judgements in derivations
> of a rule system for some logic. Often, these are λ-terms or
> variations on λ-terms. Generally, a proof term captures some of the
> structure of the derivation, although sometimes quite a bit of the
> structure is lost. I am aware of a terminological distinction between
> "Curry style" where pure λ-terms are used and "Church style" where
> type are inserted in the λ-terms. Are there any other interesting
> terminological distinctions?
>
> I think I need to define some new terminology, but I would prefer to
> reuse existing terminology if possible and if not at least avoid
> conflicts.
Carl Eastlund <carl.eastlund at gmail.com> wrote this in reply:
> I can't help you on the terminology front, but I have a question about
> your description of proof terms. As I understood it, the purpose of
> proof terms was in fact to capture the entire structure of the
> derivation, and that none was lost. Are some proof terms used
> otherwise? Can someone shed some light on this?
Here are some examples. Consider the usual Curry-style simply typed
λ‐calculus (STLC). Consider this λ-term:
M1 = λx.λy.x
Using the usual typing rules, the term M1 does not uniquely determine
the derivation, because both of the following judgements can be
derived:
M1 : ({} ⊢ a → b → a)
M1 : ({} ⊢ (c → c) → b → c → c)
(By the way, I always write the judgements with the proof term on the
left rather than in the middle because I believe that this helps
prevent certain unproductive thought patterns.)
Church-style type systems pin down more details of the derivation, but
also typically leave some details unspecified. Consider the usual
Church-style presentation of STLC. Consider the following
type-annotated variation of the term M1 from above:
M2 = λx:a.λy:b.x
Using the usual typing rules, the term M2 does not uniquely determine
the derivation, because both of the following judgements can be
derived:
M2 : ({} ⊢ a → b → a)
M2 : ({z : c} ⊢ a → b → a)
The issue here is that there can be extra unused type assumptions for
variables that are not free. The following example λ-term illustrates
a more serious issue.
M3 = λx:a.y
Because y is free in M3 and has no type annotation, for any type t
that one chooses, the following judgement is derivable:
M3 : ({y : t} ⊢ a → t)
In SLTC, this is not so important, but for Church-style System F,
Aleksy Schubert proved that the lack of type annotations on free
variables is responsible for making typability undecidable. To obtain
decidability of typability for Church-style System F, one needs to add
type annotations on all variable occurrences, so the two λ-terms above
would look as follows, where the leaf occurrences of x and y are
annotated with types.
M2' = λx:a.λy:b.x:a
N3' = λx:a.y:b
Here is another more insidious example. It is not uncommon to write
the cut typing rule as follows:
M : (A ⊢ s); N : (A,x:s ⊢ t)
------------------------------
N[x := M] : (A ⊢ t)
A system with this rule can produce both of the following derivations
for the term x. First, a simple derivation:
-----------------
x : ({x : t} ⊢ t)
Then, a complex way of getting the same result:
x : ({x : t} ⊢ t); y : ({x : t, y : t} ⊢ t)
---------------------------------------------
y[y:=x] = x : ({x : t} ⊢ t)
The more modern presentations of systems with a cut rule often use
explicit substitution syntax to avoid this ambiguity. A similar issue
arises for presentations of rules for left → elimination and left
union elimination, because many presentations of these rules also use
a meta-level substitution to specify the proof term in the conclusion
of the rule.
There are many more examples of these kinds of issues.
Martin Sulzmann <sulzmann at comp.nus.edu.sg> replied:
> The phrase "proof term" is also used in the Haskell type-class
> context in connection with building "evidence" for a type classes.
> In case you're interested I can refer you to some more
> specific papers.
While this is interesting, I think this is not really related to the
terminology issue I am interested in.
Joseph Kiniry <kiniry at acm.org> replied:
> I'm going to assume that you'll get several references to Martin-Lof's
> papers on this topic. They run from proof theoretic to philosophical,
> but have many semantic gems.
I would be interested in more details on where to look in Martin-Löf's
work for terminology about these issues.
Healfdene Goguen <hhg at research.att.com> replied:
> I don't know if you're interested in further distinctions on the
> amount of labeling of terms,
Yes, I am interested!
> but there are finer-grained distinctions
> than Curry vs. Church. Curry versus Church is a sufficient
> description of the differences in labels for type systems based on
> simple types. In dependent type systems "Church-style" is still
> understood to mean terms of the form "lambda x: A. M", but in general
> this isn't sufficient to define models, as discussed by Thomas
> Streicher in his book, "Semantics of Type Theory". I've been
> referring to terms of the form:
> Var(x, A) | lambda(x, A, B, M) | App(x, A, B, M, N)
> as "fully decorated terms", for example in my 2005 POPL paper, "A
> Syntactic Approach to Eta Equality in Type Theory".
This is exactly the kind of terminology I am looking for.
Does anyone else have any examples of terminology like this?
--
Thanks,
Joe
More information about the Types-list
mailing list