[PL-sem-jr] Fwd: [TYPES] Re: terminology for different kinds of proof terms?

[Carl Eastlund]

For those not on the Types mailing list, here's a recent message. 
Proof terms are the lambda expressions derived from a proof tree via
the Curry-Howard correspondence I gave a talk on last semester.  This
guy had some good answers to my questions about where proof terms fail
to capture the entire structure of the proof.  The essence is that the
environment (the mapping from variables to types) is not expressed in
a term (and, in Curry-style terms, neither are all of the types), but
read below for more detail.

--Carl

---------- Forwarded message ----------
From: Joe Wells <jbw at macs.hw.ac.uk>
Date: 27 Jan 2005 14:30:52 +0000
Subject: [TYPES] Re: terminology for different kinds of proof terms?
To: types at cis.upenn.edu


[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

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