Email Gateway (Aug 19 2022 at 08:25): Email Gateway (Aug 19 2022 at 08:25):From: John Munroe <munddr@gmail.com>
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
Email Gateway (Aug 19 2022 at 08:25):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Email Gateway (Aug 19 2022 at 08:45):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 30 2024 at 04:19 UTC