[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Michael Norrish]

Karl Crary writes:
 
> I think it would be interesting to prove the sort of result you're
> talking about, although I would prefer not to overload the term
> "adequacy" to refer to it.  However, I'm curious why you think that
> no one would ever attempt to prove adequacy (in the usual sense) for
> an HOL encoding.  Is there some technical obstacle, or are you just
> saying that the HOL community isn't interested in that sort of
> thing?

Well, I suppose we should first be sure that we're both singing from
the same choir-book.  

In the HOL setting, I guess that we should identify the meta-logic as
higher-order logic itself.  This is where the bulk of the proofs are
done.  The object logic is then the level of the lambda-calculus terms
(say the lambda-calculus is our area of interest) and the relations
upon them.  Once the basic type is established, for example, one might
define typing and reduction relations on the type of lambda-calculus
terms.

My understanding of what you meant by adequacy would be to show that
the concrete abstractions at the object level correspond to the
functions of the meta-level.  If this is so, then I think I revise my
original conclusion, and have worked up a solution (which is inspired
by Axiom 5 of the Gordon/Melham paper). 

Using the recursion principle for quotiented terms, it is not hard to
show that there exists a function ("adf") from object level terms to
meta-level functions and that adf is injective.  It can't be
surjective because the meta-level admits exotic functions, but that
gives us the isomorphism I believe you're after.

The function has defining clause

   adf (LAM v M) = \N. [N/v] M

where the LAM v t is the object level abstraction.  On the right,
there is a meta-level abstraction (the backslash is an ASCII lambda).  
The body of the function refers to the object level substitution
function.  

To show the existence of the isomorphism one has to show that adf is
injective.  (The isomorphism is with the non-exotic functions.)
Again, this is not so hard.

One might then go onto define the inverse of adf (call if "fad"),
knowing that its behaviour is unspecified on exotic functions.  This
function would have type 

   (term -> term) -> term

and could be treated as if it were a constructor of the object-level
type. 

One could then write the abstraction clause of the beta-reduction
relation 

   not_exotic f ==> (APP (fad f) M  --> f M)

dealing with sub-types like this (the not_exotic predicate) is enough
of a pain in HOL that doing things this way is not likely to be very
appealing.  Given that it's not hard to define well-behaved
substitution on quotients, just working with explicit substitution
functions seems easier.  (Proving the substitution lemma, for example,
is just a four-line proof: conceptually, "do induction; specify free
names to avoid; simplify".)

Michael.