Simply Typed Lambda-Calculus with a small-step, allocation semantics. 

This is an attempt to get a feel for Twelf with a problem somewhere
between the trivial simply typed lambda-calculus with a large-step
semantics (a Twelf documentation example) and Karl Crary's TALT
formalization (which is too complex to be useful for a novice).

Ultimately, we'd like to have a formalization of URAL and it's
successors.  While Greg has worked out a seemingly adequate encoding
of the core URAL type system, it remains unclear precisely how one
will invert the "resp_qual" predicate to reason about the use of
variables and values.  This is compounded by the fact that the core
URAL dynamic semantics is agnostic with respect to the substructural
qualifiers; hence, the type safety proof need never appeal to the a
qualifier to justify a preservation or progress argument.

refURAL ameliorates this deficiency somewhat, since the dynamic
semantics will (obviously) get stuck trying to read/write/swap/free a
unique reference after it has been freed.  Less obviously, the dynamic
semantics will also get stuck if a unique reference were to be
duplicated, strongly updated with one copy, and used at the old type
with the other copy.  As pointed out by the ICFP reviewers (and
pending revision into the ICFP paper), one can further instrument the
heap and heap typing so that unreachable (and, hence, manifestly
unused) linear and relevant references are a typing error.

However, refURAL is a bit too far down at the deep end of the pool for
me to jump with when I can barely swim in Twelf.  One can also
ameliorate the deciciency with core URAL's dynamic semantics by
adopting an allocation semantics that deallocates linear (and affine)
values at their uses in elimination forms.  This is Walker's approach
in ATTAPL.  Presumably, one can also instrument the store and store
typing so that unreachable linear (and relevant) values are a typing
error.  Such an immutable (modulo deallocation) store has the
attractive property that it is essentially inductive, since new values
can only point to older values, and should be somewhat easier to
formalize than a mutable heap.

Still, the combination of a substructural type system and an
allocation semantics would put me in over my head.  So, witness the
following, a type safety proof for the simply typed lambda calculus
(with unit and pairs), whose dynamic semantics is given by a
small-step, allocation semantics.

I've tried to keep the formalism as simple as possibly, but there are
a few aspects of the proof with which I am a little unhappy.


* Store Representation

As was noted on the POPLMark mailing list, modeling an abstract
machine with a store, considered as a partial map from (alpha-varying)
labels to values (which may have free occurences of those labels), is
very awkward to encode.  Karl Crary reported that it is possible to
pursue an approach where all the binders (labels) are introduced
first, then lay out the store, using a dependent type to ensure that
the number of binders equals the number of entries in the heap.
However, he found it too annoyig and resorted to non-alpha-varying
labels.

With that in mind, I've adopted the second approach, cribbing a little
from what I saw in Karl's TALT formalization.  Essentially, a store is
a list of (location, value) pairs, where locations are isomorphic to
the natural numbers:

st        : type.   %name st S.         %% store.elf
nil_st         : st.
cons_st        : loc -> val -> st -> st.

A store typing is analagous: a list of (location, type) pairs.

One normally wishes to ensure that a store does not contain
duplicate entries for the same location.  A simple means of
maintaining this invariant is to ensure that the locations in the
store are kept in sorted order, and to ensure that new locations are
greater than any current location.  I capture this invariant with a
store well-formedness judgement:

st_wf          : st -> type.
st_wf_nil           : st_wf nil_st.
st_wf_cons_nil      : st_wf (cons_st L V nil_st).
st_wf_cons_cons     : st_wf (cons_st L' V' S') ->
		      loc_lt L' L
		       -> st_wf (cons_st L V (cons_st L' V' S')).

It occured to me that one could (almost) equally well take this as
_the_ definition of a store.  And, for a time, I attempted to proceed
by always introducing a store with a proof of its well-formedness.
However, this became somewhat cumbersome, and there were relatively
few situations where I really needed the well-formedness requirement.
Also, note that induction on stores requires two cases, while
induction on store well-formedness proofs requires three cases; hence,
where it is possibly to get by with an arbitrary store, it is
expedient to do so.

Store allocation is represented by a relation:

st_alloc       : st -> val -> st -> loc -> type.
%mode st_alloc +S1 +V -S2 -L.

where, for convenience, the freshly chosen location is an output,
along with the extended store.  Location 0 is allocated when the input
store is empty; otherwise, location N+1 is allocated when the head of
the input store is location N.  A (proved) lemma is that store
allocation preserves store well-formedness ("st!alloc_preserves_wf").


* Machine Representation (or, lack thereof)

I would have liked to define a machine as a (store, expression) pair.

mach      : type.   %name mach M.
;              : st -> exp -> mach.               %infix right 20 ;.

This would have led to an elegant definition of the small-step,
allocation semantics:

==>            : mach -> mach -> type.            %infix right 10 ==>.
%mode ==> +M1 -M2.

lam_alloc_step : st_alloc S (lam_v F) S' L'
                  -> (S ; (lam_e F)) ==> (S' ; (loc_e L')).
app_ctxt1_step : (S ; E1) ==> (S' ; E1')
                  -> (S ; (app_e E1 E2)) ==> (S' ; (app_e E1' E2)).
app_ctxt2_step : (S ; E2) ==> (S' ; E2')
                  -> (S ; (app_e (loc_e L1) E2)) ==> (S' ; (app_e (loc_e L1) E2')).
app_beta_step  : st_lookup S L1 (lam_v F1')
                  -> (S ; (app_e (loc_e L1) (loc_e L2))) ==> (S' ; (F1' (loc_e L2))).
...

A natural property to expect and to check is the termination of "==>"
as logic program from input machines to output machines.  Intuitively,
termination (of the single step relation) holds because the expression
in the machine is smaller at each recursive call.  However, if I
present Twelf with the termination declaration:

%terminates M (==> M _).

it responds with the error:

Termination violation:
 ---> (S ; E1) < (S ; app E1 E2)

I understand that (S ; E1) is not a strict subterm of (S ; app E1 E2),
but it does seem that (S ; E1) is smaller than (S ; app E1 E2).  I was
unable to find any way to convey my intuition to Twelf.

There is an obvious way to avoid this: declare a four-place relation:

step           : st -> exp -> st -> exp -> type.
%mode step +S1 +E1 -S2 -E2.
...
%terminates E1 (step _ E1 _ _).

While I think of a machine as a distinct, if degenerate, syntactic
object, and would like to reflect that into the formalism in Twelf, it
is certainly not required.  I note that in TAPL's chapter on
references, Pierce does not define a typing judgement for machines of
the form |- (S, E) : (ST, T) or |- (S, E) (where the store typing and
expression type are left existentially bound).  Trying to prove
progress by induction on judgements of the form |- (S, E) runs afoul
of the same issue as above, where one wants to take |- (S, E1) as
smaller than, though not strictly a subterm of, |- (S, app_e E1 E2).


* Lambdas

I had a hard time settling on a definition of lambda expressions and
the typing judgement for lambda expressions.  I finally settled upon
the following:

exp       : type.   %name exp E.        %% exp.elf
lam_e          : (exp -> exp) -> exp.

|-var          : exp -> tp -> type.
%block |-var_block : some {T:tp} block {x:exp} {_:|-var x T}.
%worlds (|-var_block) (|-var _ _).

|-exp          : sttp -> exp -> tp -> type.
|-exp_var      : |-var E T
		  -> |-exp ST E T.
|-exp_lam      : ({x} |-var x T1 -> |-exp ST (F x) T2)
		  -> |-exp ST (lam_e F) (fn_t T1 T2).
%worlds (|-var_block) (|-exp _ _ _).

I originally tried to make headway with lambda expressions defined by:

lam_e          : (loc -> exp) -> exp.

|-loc          : sttp -> loc -> tp -> type.
%block |-loc_block : some {ST:sttp} {T:tp} block {l:loc} {_:|-loc ST l T}.
|-loc_         : sttp_lookup ST L T
		  -> |-loc ST L T.
%worlds (|-loc_block) (|-loc _ _ _).
|-exp_lam      : ({l} |-loc ST l T1 -> |-exp ST (F x) T2)
		  -> |-exp ST (lam_e F) (fn_t T1 T2).
%worlds (|-loc_block) (|-exp _ _ _).

which I had a vague hope would make it manifest that the argument to a
function must be evaluated to an allocated location before being
substituted.  Unfortunately, I seemed to be required to propagate
"|-loc_block" worlds through more relations than necessary.  I also
think that this approach would have run into problems similar to the
one described in the next few paragraphs.

Having revised the definition of lambda expressions to 

lam_e          : (exp -> exp) -> exp.

I attempted to define the typing judgement for lamba expressions as
the following:

|-exp          : sttp -> exp -> tp -> type.
%block |-exp_block : some {ST:sttp} {T:tp} block {x:exp} {_:|-exp ST x T}.
|-exp_lam      : ({x} |-exp ST x T1 -> |-exp ST (F x) T2)
		  -> |-exp ST (lam_e F) (fn_t T1 T2).
%worlds (|-exp_block) (|-exp _ _ _).

This worked quite well for a time, but I ultimately ran afoul of the
'Worlds and Weakening' problem described on the Twelf Wiki
(http://fp.logosphere.cs.cmu.edu/twelf/?n=Answers.WorldsAndWeakening).
I don't pretend to completely understand the issue, nor the solution.
Like Rob Simmons, the problem arose with coverage checking of the
weakening lemma ("sttp_weak_|-exp").  Adopting the solution given in
the wiki, I was led to introduce the "|-var" relation (with no
canonical elements) and the "|-var_block" declaration.  Now that there
are no store typings in the hypothesis of the typing judgement of the
lambda expression, the weakening lemma goes through with no problem.

But, by the conservation of grief principle, another problem arises
with the Preservation Lemma.  Specifically, the case for "app-beta"
requires the substitution of a location (expression) for the formal
argument of a lambda expression to preserve the type of the
application expression; i.e., to preserve the type of the body of the
lambda expression.  Of course, one cannot simply apply the hypothesis
of the "|-exp_lam" judgement to the argument 
("|-exp ST (loc_e L2) Tx"), since the hypothesis is phrased in terms
of "{x:exp} |-var x T".  Following the discussion on the wiki, I
simply prove the lemma that asserts that such a substitution is type
preserving:

pres_var       : ({z} |-var z Tz -> |-exp ST (F z) T) ->
                 |-exp ST E Tz
		  -> |-exp ST (F E) T -> type.

What is disappointing is that the statement and proof of the lemma has
precisely the feel of a substitution lemma, something that I thought
one avoided with higher-order abstract syntax.

In any case, the wiki also suggests that there may be limitations in
this approach, so I am curious how the solution alluded to by Susmit
Sarkar actually proceeds.

One final note about lambda expressions.  Note that I have given the
lambda expressions in 'Curry-style', with no type annotation on the
'argument'.  One would expect that adopting 'Church-style' would be a
simple syntactic change.  However, one interesting situation arises.
Coverage checking of the Preservation Lemma fails, reporting the
following missing case (slightly editted for presentation):

   {S1:st} {L1:loc} {L2:loc} {F1:exp -> exp} {ST1:sttp} {ST2:sttp} 
   {T1:tp} {T2:tp} {T3:tp}
   {X1:st_lookup S1 L1 (lam_v T2 F1)} 
   {X2:st_wf S1}
   {X3:sttp_wf ST1} 
   {DStTc1:|-st S1 ST1} 
   {X4:sttp_lookup ST1 L1 (fn_t T3 T1)}
   {X5:sttp_lookup ST1 L2 T3} 
   {X6:sttp_extend ST1 ST2}
   {DStTcWf1:|-stwf S1 ST2} 
   {DExpTc1:|-exp ST2 (F1 (loc_e L2)) T1}
   |- pres (app_beta_step X1) 
           (|-stwf_ X2 X3 DStTc1)
           (|-exp_app (|-exp_loc (|-loc_ X4)) (|-exp_loc (|-loc_ X5))) 
           X6 
           DStTcWf1
           DExpTc1.

The interesting assumptions are "X1" and "X4".  It appears that Twelf
is concerned about a situation where the lookup of a location in the
store yields a lambda value with argument type annotation T2, while
the lookup of the same location in the store typing yields a function
type with argument type T3.  This situation should be ruled out by
assumption "DStTc1", namely, that the store is typed by the store
typing.  Presumably an appropriate 'reductio ad absurdum' can be
applied, though I was somewhat suprised by how the missing case was
isolated to lambda expressions.

%% Follow-up.  Randy Pollack recently asked on the Twelf-list about
this very situation.  Karl Crary responded, noting that the solution
is to provide an inversion lemma for the "|-val_lam" rule:
http://www.twelf.org/pipermail/twelf-list/2005-May/000046.html
I've incorporated this solution into the proof.


* Inversion

One final item of note is that I ended up stating and proving two
lemmas related to the inversion of the store typing judgement.  What I
found interesting is that the LF types of these lemmas are identical,
only their modes differ:

pres_|-st_inversion 
               : |-stwf S ST ->
                 sttp_lookup ST L T ->
                 st_lookup S L V 
                  -> |-val ST V T -> type.
%mode pres_|-st_inversion +DStTcWf +SttpLookup +StLookup -DValTc.
prog_|-st_inversion 
               : |-stwf S ST ->
                 sttp_lookup ST L T 
                  -> st_lookup S L V ->
                     |-val ST V T -> type.
%mode prog_|-st_inversion +DStTcWf +SttpLookup -StLookup -DValTc.

In the proof of Preservation, I already have the assumption that the
store lookup succeeds with a value, so inversion yields the fact that
the value has the type ascribed to that location in the store typing.
In the proof of Progress, I only have the assumption that the store
typing lookup suceeds with a type, so inversion yields the fact that
the store lookup will succeed with a value of the appropriate type.

Technically, the "prog_|-st_inversion" lemma could be obtained by
composing "pres_|-st_inversion" and a simpler lemma that yields the
store lookup from the store typing lookup.  However, this 'simpler'
would have exactly the same structure as "prog_|-st_inversion", simply
discarding the value typing which is manifestly available.

The "pres_|-st_inversion" lemma is interesting as it is the one place
where I needed a 'reductio ad absurdum' argument, to rule out the
cases where the store typing lookup hits but the store lookup misses,
where the store typing lookup misses but the store lookup hits, and
where both the store typing lookup misses and the store lookup misses
but with different head locations.  Ultimately, the contradiction
always reduces to an (absurd) assumption of the form "loc_lt L L".

Also, the store and store typing well-formedness judgements are used
in the inversion lemmas to prove that a non-empty store or store
typing is an extension of its tail.


* Adequacy

I've seen the definition of 'adequate representation' enough to have
an intuition about what it is trying to establish.  But, like Twelf
proofs in general, I haven't found many examples in that are useful.
Most, like the simply typed lamdba calculus or natural deduction, are
so transparently adequate that they are ultimately useless.

While I am fairly confident that the encoding here is adequate, I
can't honestly say I know how to go about verifying that claim.  That
said, there are a couple of things of which I am slightly suspicious;
at the very least, I would like to hear an explaination of why they
don't cause any problems.

One thing concerns the "|-var" relation above.  I note that for the
'reductio ad absurdum' arguments in Twelf, one introduces an "absurd"
type with no canonical elements, lemmas that derive "absurd" from
contradictory assumptions, and lemmas that derive anything from an
"absurd" assumption.  What is slightly troublesome is the fact that
the "|-var" relation has no canonical elements, and, hence, one might
consider it isomorphic to "absurd".  Which makes the "|-exp_lam" rule

|-exp_lam      : ({x} |-var x T1 -> |-exp ST (F x) T2)
		  -> |-exp ST (lam_e F) (fn_t T1 T2).

appear to introduce a false assumption in the hypothesis.  Greg
suggests that the reason this is not problematic is the fact that the
"|-exp" relation is defined with a "|-var_block" world.  Hence, we are
allowing "|-var" as an allowable assumption, even in the absence of
any canonical elements.  But, I can't say that puts all my concerns to
rest.

Another related issue.  The vacuousity of the "|-var" relation
'breaks' coverage checking of the "|-exp" relation, in the sense that
I can leave out a typing rule for an expression form and coverage
checking succeeds.  Certainly I don't need coverage of "|-exp" to
establish the safety of the language, but it is something that I'm
naturally led to add to the declarations of the typing rules and it is
a bit disconcerting that it no longer means what I thought it meant.


* Minor Twelfisms

I don't know how often it comes up in practice, but one thing I found
annoying was the lack of any form of local term abbreviations.  For
example, here is the definition for store allocation on a non-empty
store:

st_alloc_cons  : st_alloc (cons_st (mkLoc N) V S) 
		          V' 
		          (cons_st (mkLoc (s_nat N)) V' (cons_st (mkLoc N) V S)) 
		          (mkLoc (s_nat N)).

I feel that there is a lot of repetition that obscures things.  I was
looking for some sort of syntax like:

st_alloc_cons  : let L = mkLoc N in
                 let S = cons_st L V _ in
                 let L' = mkLoc (s_nat N) in
                 let S' = cons_st L' V' S in
                 st_alloc S V' S' L'.

which I felt would make the definition clearer.

Another annoyance is the lack of actual functions, particularly on
types with a single canonical form.  For example, in the
"st_alloc_cons" definition above, I need to unwrap a location,
exposing the natural, increment the natural, and wrap back to a
location.  Whereas, knowing that "loc" has the single canonical
element

mkLoc          : nat -> loc.

it seems clear that I could write function "inc_loc" with the same
behavior, which would further simplify the definition above.  Perhaps
Carsten Schürmann's current work on Delphin is working in this
direction.

I know I could define "inc_loc" as a 'function moded' relation:

inc_loc        : loc -> loc -> type.
%mode inc_loc +L1 -L2.
inc_loc_       : inc_loc (mkLoc N) (mkLoc (s_nat N)).

But then even my 'improved' "st_alloc_cons" definition would look
like:

st_alloc_cons  : let S = cons_st L V _ in
                 let S' = cons_st L' V' S in
                 inc_loc L L'
                  -> st_alloc S V' S' L'.

which still seems overly complicated, as it introduces a hypothesis
which in turn has a single (total) cannonical element.


* Theorem Prover

I was pleasantly suprised to see that the theorem prover was able to
prove a number of lemmas that I had first proved by hand.  The theorem
prover ultimately balked at the store typing weakening lemma for
"|-val".  What is somewhat odd is that the thorem prover succeeds
without complaint on the corresponding lemma for "|-exp", and the hand
proof for "|-val" is a straightforward proof by cases.  I suppose the
subtlety that foils the theorem prover is that the case for a lambda
value requires appealing to the weaking of "|-exp" under the lambda.

The disappointing aspect of the theorem prover is that it seems that
proven theorems are not available as relations for use in by hand
proofs.  (This is a consequence of the fact that proofs are not
presently realized as logic programs?)  It would be very nice to use
the theorem prover for trivial lemmas, but be able to appeal to those
lemmas in theorems that are not provable by the theorem prover.


* Conclusion

I'm interested in hearing anyones thoughts or opinions.  I'm hoping to
add some more comments to the formalism, making it a good exemplar.
Also in that vein, I'd like to send it off to some Twelf experts for
some constructive criticism.  I also want to read through the POPLMark
Challenge solution with the insights I've gained from this endeavor.
I'm certain that it will make more sense now, though at a first
reading, it was a bit deeper than I was comfortable swimming.