[TYPES] rewriting of typed combinator expressions

[Thorsten Altenkirch]

Jeremy Dawson wrote:

>[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
>
>HI,
>
>Rewriting of combinator expressions according to the rules
>such as 
>I x -> x
>W f x -> f x x
>S x y z -> x z (y z)
>
>terminates if the terms are well-typed, but not in general.
>
>This could be proved by expressing I, W, S, etc as lambda-terms
>and using the termination of beta-reduction (for well-typed terms).
>
>But proofs to do with beta-reduction have complications to do with 
>substitution.  Can anyone give me pointers to published proofs
>of the termination of rewriting well-typed combinator expressions,
>without going via lambda-calculus and beta-reduction?
>
>Thanks for any help
>
>Jeremy Dawson
>
>  
>
Hi Jeremy,

indeed this calculus gives rise to the simplest proof using logical 
predicates. I.e. define for any type A
a set (or a predicate) SC^A (for Strongly Computable) which is a subset 
of the strongly normalizing
terms (SC^A <= SN^A) by

       SC^o = SN^o
       SC^(A -> B) = { t : SN^A | all u:SC^A . t u : SC^B }

Next we prove that t:A implies t:SC^A which has as a corollary t:SN^A by 
induction over t:A (or
the derivation of this, if you prefer). It turns out that application is 
now easy (as opposed to try to show 
directly that SN is closed under application), because if t:SC^A->B and 
t:SC^A then by the very definition of SC^(A->B)
t u : SC^B. However, a bit more work is required to see that all the 
combinators are in SC, e.g. to show
that I : SC^(A -> A) we first note that I is in SN^(A->A) - no rule 
applies - and it remains to show that given
t : SC^A we have that I t : SC^A. To establish this we need a key lemma: 
Given t:SN^C for any C and
for all one step reducts t ->> u we have that u:SC^C then t:SC^C (by 
induction over C). Once we have
this lemma we notice that a reduct of I t is either t or I t' where t 
--> t' and using the lemma and the fact that
SN is inductively defined we are able to show I t:SC^A. The cases for 
the other combinators proceed in a
similar fashion. []

Some remarks:

I believe that one-step reduction is a bit of a historical mistake: who 
executes their programs by
rewriting them to normal forms (maybe mathematicans)? More realistic is 
to define a big-step semantics which
can be easily turned into a functional program which can be further 
turned into a machine (by making it tail
recursive) . Interestingly, the SN-proof becomes even simpler because 
the lemma is easier, e.g see my recent
lecture notes for more details 
(http://www.cs.nott.ac.uk/~txa/publ/mgs04.pdf).

Another alternative is to use NBE which gives rise
an even nicer construction (i.e. a program with its correctnes proof) 
for normalisation. This is spelled out in
Dybjer's and Coquand's article, see _ 
<http://www.cs.chalmers.se/%7Epeterd/papers/GlueingTypes93.ps.gz>_
http://www.cs.chalmers.se/~peterd/papers/GlueingTypes93.ps.gz

Introducing lambda as such doesn't complicate the construction, even 
though we have to prove a substitution
lemma (showing that SC is closed under substitution). What *does* 
complicate the construction is to introduce
the xi-rule (reduction can go under lambda) which leads to "neutral 
terms", i.e. normal forms which can be
no further reduced due to the presence of variables (e.g. like x t1 t2 
.., where ti are normal). In the
classical proof this is captured by using a logical predicates in the 
"oper term model" where terms may have
different contexts (sets of typed free variables) and by establishing an 
extra lemma showing that all
neutral terms are SC. To me this always seemed a bit adhoc, the proper 
way is to realize that SC is now
a Kripke logical predicates (or use presheaves for NBE). The whole story 
gets further complicated if you introduce
coproducts which lead to sheaf semantics (see 
http://www.cs.nott.ac.uk/~txa/publ/lics01.pdf)
or Grothendieck logical predicates for reduction, even though nobody has 
spelled out
the latter (there is a reduction based proof in Neil Ghani's PhD, though).

Cheers,
Thorsten



   



This message has been scanned but we cannot guarantee that it and any
attachments are free from viruses or other damaging content: you are
advised to perform your own checks.  Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.