[TYPES] HOAS versus meta reasoning

[Andrei Popescu]

Thank you for your explanations!  

>> --- On Thu, 11/13/08, Karl Crary <crary at cs.cmu.edu> wrote:
>> Their framework also shows that the concern that is sometimes raised 
>> over negative instances arising in HOAS is really a red herring.  

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.)

A "constructor" like 
-- lam : (exp -> exp) -> exp.
may be fallacious in classical logic, but one may hope that it would be 
valid (i.e., actually representing a constructor) in other logics.  
Of course, changing/restricting
 the function space is another possible solution (or this may be part of 
the solution).  

This "naive" hope driven style of inquiry becomes sharper, in my 
opinion, when we move from 
representing syntax to representing inference, and I think the latter is 
an equally important aspect of HOAS which unfortunately is not transparent
in the name "HOAS". (By the way, approaches around weak HOAS, including Nominal Logic, do not seem to address this issue at all.)  
Consider a typing system with a familiar rule 
for typing abstraction, like

Gamma, x : A |- Y : B
----------------------------
Gamma |- Lam(x:A,Y) : A -> B

In idealized HOAS, one would represent it as something like

(All x. typeOf(x,A) => typeOf(Y x,B)) =>
typeOf(Lam(A,Y), Arrow(A,B))     (*) 

(where we may assume that Lam is now an operator of type 
(Term -o-> Term) -> Term, for some appropriate choice of 
the space Term -o-> Term that comes 
with an appropriate application destructor.)  

The question is of course not whether the above clause is sound 
in a classical logic for the represented system (typically it will not 
be sound, and one reason for this is that it will type anything to 
an arrow type with uninhabited source), but: 

When and where is it sound? 

And, if so:

When and where can it be viewed as something like an inductive clause 
(just like its object-level counterpart)?  

The answers in the style of the Miller-McDowell and Twelf approaches are 
instances of the following: consider a further 
meta-level layer and from there you can regard this clause 
(via its associated 
rule on sequents in the representation logic) as an inductive clause.  
However, isn't this shifting the burden of handling contexts from the contexts of the object logic to the ones of the representation logic?   

Andrei Popescu

 





--- On Thu, 11/13/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: Thursday, November 13, 2008, 10:13 PM
> I see.  You should probably look at Licata, Harper, and
> Zeilberger's paper from the most latest LICS.  They show
> that you can sort (one might say tame) the HOAS issues by
> taking a view based in focusing (which arises from theorem
> proving).
> 
> The basic idea to focusing is to sort the connectives into
> positive and negative.  Positive connectives are eliminated
> via pattern matching, while negative connectives are
> introduced via pattern matching.  For example, sums are
> positive because they are eliminated using pattern matching,
> but functions are negative because they are introduced using
> pattern matching (on the argument).  Products can be taken
> either way, resulting in two different connectives.
> (Equivalently, you can view positive connectives as ones
> with a closed-scope elimination form and negative
> connectives as ones with an open-scope elimination form.)
> 
> They observe that the representational arrow used in HOAS
> is not the usual negative function space, but a *positive*
> function space.  The positivity of the function space
> ensures that the function is parametric, which higher-order
> representations depend on.  In essence, A -pos-> B refers
> to a B that is constructed using a new introduction form for
> A.  (Note that A must be atomic; otherwise positive
> functions would be creating new intro forms for
> connectives.)
> 
> Functions that analyze their arguments employ the usual
> negative function space.  Although most existing LF-based
> systems have (what we can now recognize as) negative
> functions only at a meta-level, there's no reason it
> must be so.  We can integrate positive and negative
> functions into the same system, and there's good reason
> to do so.
> 
> When you do so, the two function spaces can interact in
> interesting and surprising ways.  In short, some of the
> structural properties that one expects can fail when the two
> are combined.  (I suspect this is the sort of thing you are
> looking to tame.)  Licata, et al.'s framework shows
> exactly when/how this happens, and what you need to do to if
> you want to prevent it from happening.
> 
> Their framework also shows that the concern that is
> sometimes raised over negative instances arising in HOAS is
> really a red herring.  The problem, as I understand it, is
> as follows:  Suppose I take the higher-order representation
> of the lambda calculus:
> 
> lam : (exp -> exp) -> exp.
> app : exp -> exp -> exp.
> 
> and try to make it into a recursive definition.  Then I
> obtain something like:
> 
> mu X . (X -> X) + (X * X)
> 
> and this doesn't work the way it is supposed to,
> because of the negative occurrence of X.  Consequently, you
> cannot use HOAS in this manner.
> 
> Some people find this mysterious, but the mystery
> disappears when you consider which arrow is being used.  If
> I use the negative arrow this can be fine, but it has
> nothing to do with HOAS, which relies on the positive arrow.
>  If, on the other hand, I use the positive arrow, then this
> is ill-formed (even if we have recursive types), because the
> domain of a positive function has to be atomic, and
> therefore cannot be the type variable X.
> 
>    -- Karl Crary
> 
> 
> 
> Andrei Popescu wrote:
> > Dear Andrew and Karl, 
> > I thank you very much for your comments and
> references.  
> > To answer Karl's question, I used the word
> "taming" because, as far as I see, the interaction
> between meta-reasoning (by which I understand reasoning
> about the object system) and HOAS is a wild issue.  Going
> back one level and (case-)analyzing the meta-logic inference
> itself in a meta-meta logic seems like an elegant, but
> extreme measure to take  -- for one thing, it breaks the
> ties with more conventional frameworks for developing
> mathematics, such as the ones of Coq, Isabelle/HOL or PVS,
> where a working mathematician feels immediately comfortable
> (thanks to the standard foundations), and where many
> libraries of theories are available. Staying in a
> conventional framework, on the other hand, requires
> compromises on the hassle-free (i.e., typing-context-free,
> substitution-free, bound-variables-free etc.) aspect of the
> representation.  I was not looking for taming any aspect in
> particular, but for getting a picture of the recent progress
> within the above approaches and maybe others in between.  
> > Regards,  Andrei Popescu  
> > 
> >