[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Karl Crary]

Hi Michael,

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?

    -- Karl Crary


Michael Norrish wrote:
> I don't think anyone would ever attempt the project you are describing
> for HOL.  Rather, we would prove what I think might be called an
> adequacy result entirely at the object level.  It is trivial to
> establish a type of first order, algebraic terms corresponding to the
> named syntax with explicit free variables, and not identified up to
> alpha-equivalence.  I think this is the type that we all accept as the
> fundamental bedrock, to which we can all revert if we must, however
> unpleasant its properties.  This is the type for which notions of
> recursion and induction are uncontroversial.
>
>