[MetaPRL Users] some metaprl questions

[Aleksey Nogin]

On 21.06.2007 14:41, James Caldwell wrote:

> 1.) I can seem to find Fold or FoldC .... there is something about 
> folding but I need to provide a conversion to do so?  Not sure how to do 
> this, in Nuprl I can just name the definition I'd like to fold ( e.g. 
> FoldC `foo`)

In MetaPRL, we normally define a fold conversional dual to unfold using 
makeFoldC (which takes a term schema and an unfold conversion as 
arguments). For one-time fold creation on the command line, you can also 
use foldC. A Nuprl-style generic [un]fold conversion is probably a good 
idea, but we have never implemented it.

> 2.) I'm having some trouble with squiggle -- which I never really used 
> in Nuprl.  Do I understand correctly that t1 ~ t2 holds if I can rewrite 
> t1 and t2 into a common form? 

Yes, squiggle is a computational+defintional equality. Essentially, in 
MetaPRL's ITT it's a conditional form of the "<-->" meta-relation.

> If so, this would seem to mean that (for 
> functions anyway) this is a finer equality e.g.  there may be 
> extensionally equal functions which can never be reduced to alpha 
> equivalent forms.

Yes.

> For example, you 
> seem to support (via rewriteC) a conversional for rewriting with 
> squiggle, but don't have a similar one for real equality.   Probably I'm 
> just missing it.

For equality, we normally use substT (which is resource-driven and can 
handle both squiggle and normal equalities) instead of rewriting. substT 
also knows how squiggle reasoning under a binding (lambda_sqsubst* stuff 
in Itt_struct2).

> 3.)  In the meta-part of metaprl -- we can write something like C[x]  
> where C is a context ... but surely there is nothing I can ever do to 
> show functionality for the slot in C.  This would seem to mean that we 
> can't use hypSubstT.  Is this right?  I guess we'd be OK with squiggle 
> here though because of the computation rule.

When you use contexts in theorem statements, you often need to have add 
the appropriate wf assumption to that theorem. Once you do that, you can 
use substT.

BTW, the "meta" in MetaPRL refers to the ability to define arbitrary 
logical theories and calculi and relate them to each other. The contexts 
language is just one of the mechanisms for making that happen.

Aleksey

-- 
Aleksey Nogin, Research Scientist
Advanced Technologies Department, Information & System Sciences Lab
HRL Laboratories, LLC, Malibu, CA