[TYPES] HOAS versus meta reasoning

[Andrei Popescu]

1) I did not use the word "naive" pejoratively.  (True, because of its 
connotation, I should have avoided this word altogether.)  I meant it 
as referring to a pure, not necessarily (or immediately) mathematical 
(or mathematically consistent) idea, just like Cantor's "naive" 
notion of a set described by 
comprehension. I certainly did not want to sound as if I am trying to 
trivialize the idea (although, unavoidably, I have 
reduced it by casting it into my own understanding).   
Also, I was not trying to peer (in any sense of the word :) ) into the 
mind of the LF creators, but rather into the mind of a common 
working-class person 
that works at representing logics and reasoning about 
and wants to have her/his job 
simplified.   

2) LF was designed for encoding logics for the purpose of reasoning *in* 
these logics. It does this job beautifully for structural logics, 
and is also able to do this for some non- (or less-) structural logics. 
Most logics in current use fall in these categories.  End of the story.  
I have no questions here.  Encoding a logic in a meta-logic higher-order-
abstract-syntactically 
proceeds axiomatically (stating axioms in the meta-logic).  This approach 
(LF, Pfenning and Elliott, (generic) Isabelle, etc.) 
uses frameworks which are, as Karl 
Crary reminded me, very weak purposely for accommodating logic 
definitions.  

In the above light, thinking of HOAS as a mechanism for encoding a logic 
L in a meta-logic M for reasoning *in L*, there is nothing of the sort 
of things I have talked about.  My "psychological interpretation" of 
the HOAS idea only makes sense after one poses the question 
of meta-reasoning 
*about L*, hopefully in M or a natural extension of M.  
For this, one needs to induct in M 
about L-inferences.  One way to try to achieve this is by replacing M 
with a 
stronger (more "committed") logic M' so to allow induction principles 
and try to use the same (or a similar) style of representation for L in M' 
as for L in M, retaining the HOAS flavor (and convenience).  
(Having his precious M already accommodating adequacy nicely,  
one may alternatively  prefer to leave M 
unaltered and take M' as a 
meta-logic for M rather than as an extension of M.  Then reasoning about 
L-inferences becomes reasoning in M' about M-inferences.  This preserves 
the HOAS nature of syntax encoding, but, as far as I see,   
re-introduces a level of indirection in dealing with inferences 
present in non-HOAS encodings -- I detail this below at point 3. )  

But one does not need to go through logical frameworks (i.e., 
through the notion of representing L for the purpose of 
reasoning *in L*)  
to reach the latter idea. Thus, for instance, one can start 
directly with a stronger logic M' and try to HOAS-represent L in it 
definitionally (or partly definitionally, partly axiomatically), 
rather than entirely axiomatically.   (And this has been done.)  
Typically M' shall be strong enough so that it is able to define any 
(recursively specifiable) logic in a way that mirrors 
the informal definition of L (without employing HOAS) -- e.g., 
if M' is HOL or ZF and L is simply-typed 
lambda calculus, then 
the representation of L in M' would be the standard definition 
of this calculus in M' (with alpha-equivalence and substitution defined 
as usual, etc.).  In such a logic M' (say, for now, that M' is HOL), 
since 
one has the standard definition to refer to, one can 
now ask my question: 

For the term "lambda x : T. E", can I assume that 
"lambda" is really function abstraction (so that in HOL lambda-terms 
will be functions, and, regarded from a meta-logic for which both HOL 
and L are objects, so that the L-bindings are captured by HOL-bindings)? 

(The answer to the question may require modification of the 
principles of the logic and/or of the notion of a function, etc.) 

The above statement of the goal of HOAS-representing syntax 
has in itself the assumption that one will also 
want to reason *about* this syntax.  What turned out, due to my 
not very careful choice of the words, as 
a conjecture that this was 
the original motivation behind HOAS is indeed anachronistic, 
since, indeed, 
an approach that first visits logical frameworks 
already has a HOAS representation of syntax and wants 
to extend it with inductive reasoning.  


3) Regarding the situation of M' being a meta-logic for M rather than 
an extension of M (or M itself).  I think this retains the 
HOAS convenience 
for dealing with syntax (as Dan Licata pointed out), but loses,   
to some extent, the convenience of dealing with inference/judgments.  
I can best explain what I mean by taking an object-logic 
example that does not possess any bindings -- this symbolizes a 
situation where the syntax representation has already been dealt 
with adequately, and we may focus on inference.  The object system 
L is the following:

Syntax: 

n ::= 0 | S(n)
Gamma ::= [] | Gamma,n

Inference: 

Gamma |- 0

Gamma,n |-  n 

Gamma |- n
-----------
Gamma,m |- n

Gamma |- n 
--------------
Gamma |- S(S(n))

Since L is a structural "logic", we may encode this 
axiomatically in blank intuitionistic 
HOL (or, alternatively, in an explicit-proof-term 
fashion, in LF)  as follows:

type nat
op S : nat --> nat 

Deduce(0) 

Deduce(n) => Deduce(S(n))

This is fine (adequate) if we want to reason *in L*.   For being 
able to reason *about L* while retaining a similar representation, one 
may assume (a carefully chosen version of) HOL with induction 
and recursion  principles included and:
-- use the HOL type nat of natural numbers for encoding the syntax
-- use a predicate Deduce : nat --> bool defined 
recursively by the above axioms (now regarded as inductive clauses).  

Now, if an adequacy result includes at least the following:

[] |- n  (in L)   iff   HOL |- Deduce(n)  

then we would be able to reason in HOL about L (at least w.r.t. 
properties holding in L with empty context), while retaining a 
shallow encoding of L-inference (and not only of L-syntax).  

On the other hand, if we choose to keep the original blank HOL (which 
allows axiomatic adequacy) and move one level up to a meta logic M' 
that accommodates induction over HOL inferences, then we would not 
speak of a predicate "Deduce",  but rather of a predicate 
"HOL |- Deduce(n)", which does not seem more convenient than 
using directly 
a definition of L in M' and speak about a predicate "[] |- n".  
This approach keeps the HOAS encoding of syntax, but looses 
the HOAS-encoding of inference.   

True, my example of a logic L does not illustrate the problem of 
judgments whose natural 
shallow embedding has negative occurrences of atomic formulas 
that seem to stand against inductive interpretations.    
Moreover, properties of L 
that require the consideration of typing contexts 
essentially, such as: "If Gamma |- n, then there exists Gamma' that 
includes Gamma and has even cardinality such that Gamma' |- n", 
cannot hope 
for a formulation in a context-free representation, just like 
properties that refer to bindings and free variables cannot be formulated 
in a HOAS representation.  Probably these are reasons for 
not going after a shallow embedding of inference after all.  
Regarding the second aspect though: many properties of interest, 
including type preservation and normalization,  
have the empty-context case holding the essence of the property 
(and the main difficulty in a presumptive proof), with the extension of 
the result to a contextual version being a mere formality.   

Regards and apologies for the length of this message, 
   Andrei  





--- On Tue, 11/18/08, Karl Crary <crary at cs.cmu.edu> wrote:

> From: Karl Crary <crary at cs.cmu.edu>
> Subject: Re: [TYPES] HOAS versus meta reasoning
> To: uuomul at yahoo.com
> Cc: types-list at lists.seas.upenn.edu
> Date: Tuesday, November 18, 2008, 6:01 PM
> Well, let me just say that rather than try to peer into the
> mind of the authors of LF, I would prefer to let the
> mathematics stand for itself.  I'm not aware that the
> theory of adequacy developed in LF was somehow deficient.
> 
> It's been known from the start that the power of LF
> stemmed from its apparent weakness.  In the years since LF
> was invented, there has been a lot of effort to carry out
> the LF methodology (now often called higher-order abstract
> syntax, or higher-order representations) in a stronger
> settting, in order to use higher-order representations and
> simultaneously do something else.  That's what I thought
> we were talking about.
> 
>    -- Karl Crary
> 
> 
> Andrei Popescu wrote:
> > I would not call the above neither concern, nor a red
> herring, but rather state it in the form of a
> "naive" hope.  Without trying to invent
> pseudo-paradoxes, I would just like to point that the idea
> behind the HOAS paradigm (as I see it) was in itself
> something that looked like a naive hope, coming from the
> "logical fallacy" of confusing the object-level
> with the meta-level: 
> > "When I consider the lambda term <<lambda
> x. E>> why can't I assume that "lambda"
> is not just a representation of a function abstraction, but
> it *is precisely function abstraction*? "
> > 
> > Of course, this "naive" hope has received
> sophisticated solutions,  and the references of this thread
> witness this.  (A similar situation being the "naive,
> non-mathematical" equations written
> > by Christopher Strachey to express the meaning of
> programs that later received mathematical justifications
> from the domain theory of Dana Scott.)
> >