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

[James Caldwell]

Thanks ... that explains it.

Jim

On 6/12/07, Aleksey Nogin <anogin at hrl.com> wrote:
>
> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.metaprl.org/pipermail/metaprl-users/attachments/20070613/c5251156/attachment.html