[MetaPRL Users] any(x) \in T and extracts in general.

[Aleksey Nogin]

On 12.06.2007 16:59, James Caldwell wrote:

> I don't see the "any" term declared in itt_void (where I sort of expect 
> to see it)   Is it declared somewhere else ?  or is it not used?

It's not used. We have an informal tradition of using the "it" term (AKA 
"Ax" in NuPRL) whenever we need an arbitrary closed term. In particular, 
the Itt_void.voidElimination rule uses "it" as its extract.

> define unfoldInd 
[...]
> (/n/ < 0) ⇒ /Ind/(/n/) = ·
[...]
> I sort of expect the the case for n<0 to say something like  ((n<0) ⇒ 
> /Ind/(/n/) = any(n)).

Same deal here - the "it" term is used. I agree that it might make sense 
to use a special custom term in each of these cases (although it does 
not really matter), however IMHO having that term parameterized over 
some argument does not make much sense - it would only suggest a 
dependency, where none exist and slow things down.

> We haven't played with extracts yet ... and I guess i don't even really 
> know where to look for them ...  if any isn't there ... what would the 
> extract be for e.g . void_elimination? 

Every axiom ("prim" rule) in MetaPRL must have an extract. While there 
is a way to define a default extract as a way of not requiring explicit 
extract specifications (for theories that do not care), this is not used 
in ITT. All the "prim" rules in ITT do have an extract - this is the 
stuff after the "=" in the ".ml" files. (This syntax is used because the 
statement of the rule is a rule "type", while the extract is the rule 
"implementation").

Aleksey

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