[Prev][Next][Index][Thread]
Re: Lambda Calculus with Explicit Substitution as a term assignment?

To: sanjiva@brics.dk (Sanjiva Prasad)

Subject: Re: Lambda Calculus with Explicit Substitution as a term assignment?

From: Rene Vestergaard <jrvest@cee.hw.ac.uk>

Date: Wed, 23 Sep 1998 14:10:16 +0100 (BST)

Cc: types@cis.upenn.edu

InReplyTo: <199809211311.JAA20459@saul.cis.upenn.edu> from "Sanjiva Prasad" at Sep 21, 98 03:05:32 pm
> Is there a propositionsastypes, programsasproofs account where a
> lambdacalculus with explicit substitution serves as the term
> assignment language for a suitable intuitionistic logic? Any pointers
> to relevant papers will be appreciated.
Yes. I recently wrote a technical report entitled "The Cut Rule and
Explicit Substitutions" in which I construct such calculi from known
logical deduction style inference systems. It essentially shows that
there is a tight connection between propagation of the cut rule(s) and
propagation of explicit substitutions a` la \s, \t, and \xgc. It also
has quite a few references to earlier work that addresses similar (but
not the same!) issues. It is available from
http://www.cee.hw.ac.uk/~jrvest/Writings/writings.html
In a forthcoming article (tentatively called "The Correspondence
between CutPropagation, Explicit Substitutions, and \betareduction")
I prove how a variant of the ZuckerPottinger(Mints) epimorphism
[1,2,3] factors through explicit substitutions. That is, I prove that
\s and \t (and \xgc?) can be obtained as homomorphic images of cut
propagation. These calculi with explicit substitution produce, in
turn, \betareduction as a homomorphic image.
Regards
/R
PS! I noticed, Sanjiva, that you are at BRICS. Olivier Danvy should be
able to give you further information on these issues.
[1] J. Zucker: "The Correspondence between CutElimination and
Normalization, Part I". Annals of Mathematical Logic, 7:1112
(1974). NorthHolland.
[2] G. Pottinger: "Normalization as a Homomorphic Image of
CutElimination". Annals of Mathematical Logic, 12:323357
(1977). NorthHolland.
[3] G. Mints: "Normal Forms for Sequent Derivations". In P. Odifreddi
(ed.): "Kreiseliana  about and around Georg Kreisel" (1996).
A.K. Peters Publishers.