The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 15.11.2012 08:32, schrieb Jonas Oberhauser:
> Am 15.11.2012 02:51, schrieb Norman Danner:
> > Hello list,
> >
> > I am looking for a development of the simply-typed lambda calculus 
> > that I could look at, as I'm having some trouble doing this on my 
> > own.  I suspect my difficulties are not deep.  What I'm looking for 
> > is a development along the following lines:
> >
> > 1. A definition of expressions (nothing complicated; just variables,
> >    natural number constants, abstraction, and application).
> > 2. A definition of type (nothing complicated; just N and arrow types).
> > 3. A notion of type context.
> > 4. A definition of 'typed G t tau', where Pi : typed G t tau means that
> >    Pi is a derivation that t has type tau under type context G (below,
> >    G |- t : tau).
> > 5. A notion of substitution on expressions.
> > 6. A proof that if G, x : sigma |- t : tau and G |- s : sigma, then
> >    G |- t[s/x] : tau.
> > 7. The standard full-function-space denotational semantics using nat
> >    and -> to interpret N and arrow types, where den Pi xi is the
> >    denotation of (the typing of) the expression t under environment
> >    xi (i.e., really a definition of
> >    den {G} {t} {tau} (Pi : typed G t tau) xi).
> > 8. A proof that if Pi is a derivation of G |- t[s/x] : tau obtained
> >    from derivations Pi_t of G, x:sigma |- t:tau and
> >    Pi_s of G |- s:sigma, then
> >    den Pi xi = den Pi_t (xi[x |-> den Pi_s xi]).
> >
> > I can do 1-7 without much difficulty.  8 is killing me.  I assume it 
> > is because I am doing something sub-optimally somewhere in 1-7.
> >
> > I'm sure I'm not the first person to try to do this, and I think the 
> > most efficient way to solve my difficulties is to see it done right.  
> > I would be grateful for pointers to solutions. Thanks!
> >
> >     - Norman
> Here are the first six (+reduction). I formalized confluence and 
> termination using these files so I think they are sound. A lot of this 
> has been done by Chad and Smolka.
>
> What you mean by 7 I do not know. Do you mean a function from term to 
> Type where [type e t N] implies [[t]] = interpret N and [type e t (T 
> -> U)] implies [[t]] = (interpret T) -> interpret U ?
> Kind regards, jonas

Ah in fact this formalization does not have natural number constants, 
but if you want to interpret N by nat then just increase the context by 
some variable of N. I don't think this changes much.

Also note the use of de Bruijn indices for variables.

jonas