[FOM] Simply Typed Lambda Calculus
ilitzroth at gmail.com
Mon Jan 14 06:04:33 EST 2008
2008/1/12, Steven Obua <obua at in.tum.de>:
> I have the following question concerning the simply typed
> (non-polymorphic) lambda calculus with constants and axioms for those
> The axioms are all of the form p = t, where p is a linear pattern and
> all the free variables in t are bound by p. All the axioms are typed.
> Assume that I have two terms A and B, both typed.
> Assume further that I forget now about all types and use beta , eta
> conversions and the axioms as if I would do in untyped lambda calculus.
> Doing this, I manage to get from A to B.
> My question is, can I therefore also get from A to B if I DO NOT forget
> about the types but respect them? In particular, certain eta
> abstractions might not be possible that I could use
> in the untyped setting but not in the typed setting.
Hindley "Basic Simple Type Theory"
2C1: Subject Reduction Theorem:
if Context |- term1:type and term1 |> term2 where |> stands for beta
then Context |- term2:type.
The reverse is not true: if term2 is typed it could have com from a
nontyped term (which is
why no attempt is made at defining a typed convertability relation as
he explains in chapter
5 of the same work).
Adding axioms does not change this since your axioms are typed.
> I guess for type theorists this is a no-brainer. It would be great if
> someone could point me to an answer of this question in the literature.
I am not a type theorist but a c++ programmer. So you might want to check
the literature yourself and/or wait for the opinion of a real expert.
More information about the FOM