[TYPES] Re: terminology for different kinds of proof terms?

[Joe Wells]

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