%{{
# Weak head normalization for simply-typed lambda calculus
This example follows the proof presented in
Cave and Pientka[2013].
First, let's define a simply typed λ-calculus with one type:
}}%
LF tp : type =
| b : tp
| arr : tp -> tp -> tp
;
--name tp T.
tm : tp -> type. --name tm E.
app : tm (arr T S) -> tm T -> tm S.
lam : (tm T -> tm S) -> tm (arr T S).
c : tm b.
%{{ The type `tm` defines our family of simply-typed lambda terms
indexed by their type as an LF signature. In typical higher-order
abstract syntax (HOAS) fashion, lambda abstraction takes a function
representing the abstraction of a term over a variable. There is no
case for variables, as they are treated implicitly in HOAS.
We now encode the step relation of the operational semantics. In
particular, we create the `step` type indexed by two terms that
represent each step of the computation.
}}%
step : tm A → tm A → type.
beta : step (app (lam M) N) (M N).
stepapp : step M M' -> step (app M N) (app M' N).
%{{Notice how the `beta` rule re-uses the LF notion of substitution by
computing the application of `M` to `N`.
Finally, we define:
- a multiple step reduction `mstep`.
- values `val`
- `halts` to encode that a term halts if it steps into a value.
}}%
mstep : tm A -> tm A -> type. --name mstep S.
refl : mstep M M.
onestep : step M M' -> mstep M' M'' -> mstep M M''.
val : tm A -> type. --name val V.
val/c : val c.
val/lam : val (lam M).
halts : tm A -> type. --name halts H.
halts/m : mstep M M' -> val M' -> halts M.
%{{
## Reducibility
Reducibility cannot be directly encoded at the LF layer, since it
involves a strong, computational function space. Hence we move to the
computation layer of Beluga, and employ an indexed recursive
type. Contextual LF objects and contexts which are embedded into
computation-level types and programs are written inside `[ ]`.
}}%
stratified Reduce : {A:[⊢ tp]}{M:[ |- tm A]} ctype =
| I : [ |- halts M] -> Reduce [ ⊢ b ] [ |- M]
| Arr : [ |- halts M] ->
({N:[ |- tm A]} Reduce [ ⊢ A ] [ |- N] -> Reduce [ ⊢ B ] [ |- app M N])
-> Reduce [ ⊢ arr A B ] [ |- M]
;
%{{
A term of type `i` is reducible if it halts, and a `term M` of type
`arr A B` is reducible if it halts, and moreover for every reducible
`N` of type `A`, the application `app M N` is reducible. We write
`{N:[.tm A]}` for explicit Π-quantification over `N`, a closed term
of type `A`. To the left of the turnstile in `[|- tm A]` is where one
writes the context the term is defined in – in this case, it is empty.
In this definition, the arrows represent the usual computational
function space, not the weak function space of LF. We note that this
definition is not (strictly) positive, since `Reduce` appears to the
left of an arrow in the `Arr` case. Allowing unrestricted such
definitions destroys the soundness of our system. Here we note that
this definition is stratified by the type: the recursive occurrences
of `Reduce` are at types `A` and `B` which are smaller than `arr A B`.
`Reduce` is defined by induction on the type of the reducible
term(additionally this is why we cannot leave the type implicit).
Now, we need to prove some more or less trivial lemmas that are
usually omitted in paper presentations.
First, we prove that halts is closed under expansion in the `halts_step` lemma.
}}%
rec halts_step : {S:[ |- step M M']} [ |- halts M'] -> [ |- halts M] =
mlam S ⇒ fn h =>
let [ |- halts/m MS' V] = h in
[ |- halts/m (onestep S MS') V]
;
%{{
Next we prove closure of Reduce under expansion. This follows the
handwritten proof, proceeding by induction on the type A which is an
implicit argument. In the base case we appeal to `halts_step`, while
in the `Arr` case we must also appeal to the induction hypothesis at
the range type, going inside the function position of applications.
}}%
rec bwd_closed : {S:[ |- step M M']} Reduce [|- T] [ |- M'] -> Reduce [|- T] [ |- M] =
mlam MS => fn r => case r of
| I ha => I (halts_step [ |- MS] ha)
| Arr ha f => Arr (halts_step [ |- MS] ha)
(mlam N => fn rn =>
bwd_closed [ |- stepapp MS] (f [ |- N] rn))
;
%{{
The trivial fact that reducible terms halt has a corresponding
trivial proof, analyzing the construction of the the proof of
'Reduce[|- T] [|- M]'
}}%
rec reduce_halts : Reduce [|- T] [ |- M] -> [ |- halts M] =
fn r => case r of
| I h => h
| Arr h f => h
;
%{{
# Reducibility of substitutions
}}%
schema ctx = tm T;
inductive RedSub : {g:ctx}{#S:[ |- g]} ctype =
| Nil : RedSub [ ] [ |- ^ ]
| Dot : RedSub [g] [ |- #S[^] ] → Reduce [|- A] [ |- M]
→ RedSub [g, x:tm A[]] [ |- #S,M ]
;
rec lookup : {g:ctx}{#p:[g |- tm A[]]}RedSub [g] [ |- #S[^]] -> Reduce [|- A] [ |- #p[#S]] =
mlam g => mlam #p => fn rs => case [g |- #p] of
| [g',x:tm A |- x] => let (Dot rs' rN) = rs in rN
| [g',x:tm A |- #q[..]] => let Dot rs' rN = rs in
lookup [g'] [g' |- #q] rs'
;
%{{
# Main theorem
}}%
rec main : {g:ctx}{M:[g |- tm A[]]} RedSub [g] [ |- #S[^]] -> Reduce [|- A] [ |- M[#S]] =
mlam g => mlam M => fn rs => case [g |- M] of
| [g |- #p] => lookup [g] [g |- #p] rs
| [g |- lam (\x. M1)] =>
Arr [ |- halts/m refl val/lam]
(mlam N => fn rN =>
bwd_closed [ |- beta] (main [g,x:tm _] [g,x |- M1] (Dot rs rN)))
| [g |- app M1 M2] =>
let Arr ha f = main [g] [g |- M1] rs in
f [ |- _ ] (main [g] [g |- M2] rs)
| [g' |- c] => I [ |- halts/m refl val/c]
;
rec weakNorm : {M:[ |- tm A]} [ |- halts M] =
mlam M => reduce_halts (main [] [ |- M] Nil)
;