Re: [isabelle] Naive question about tactics and Pure



I think there is one more level: the ML level. You can do things on the ML level that you cannot do inside Pure or any object logic. Tactics are implemented on the ML level. Maybe there is no clear-cut border between Pure and the ML level. But I rather think about the former as a formal logic and the latter as a programming language (which it is).

To be a bit more precise (I hope). Everything origins from the ML level, since it is implemented in the programming language ML, but the part which I would call Pure (concerned with the implementation of a minimal higher-order logic that serves as logical framework for arbitrary object logics) is not whole of ML, but just some specific types and functions that serve as an interface.

Hence when you do anything in Pure it corresponds to some function call in ML and when you call ML functions from the specific interface it corresponds to some manipulation of Pure terms (which might or might not be expressible in the logic itself). But there is definitely a large space of ML functions that is not related to Pure.

Hope this makes any sense.

cheers

chris

On 08/28/2012 08:04 AM, John Munroe wrote:
Hi,

I have a rather naive question about the use of terminology. AFAIK,
tactics are implemented in the meta-level and the meta-level language
in Isabelle is Pure. So is it correct to say that "tactics are written
in Pure"?

Thanks

John







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.