Re: [isabelle] Naive question about tactics and Pure



On Tue, 28 Aug 2012, Christian Sternagel wrote:

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.

See also this thread:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-April/msg00066.html

Saying "ML level" suggests that it is somehow below other things, but it is in fact intertwined in a more sophisticated manner. This explains the preferred terminolgy "Isabelle/ML", "Isabelle/Isar" etc. without any leveling.


	Makarius





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