[FOM] Simply Typed Lambda Calculus

[immanuel litzroth]

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
> constants.
> 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
eta reduction
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.
Greetz
Immanuel