Re: [isabelle] Macro to comment and uncomment selected text so I don't get error?
On 8/9/2012 10:26 AM, Gottfried Barrow wrote:
There's "the self-defining self-embedding game of formal languages",
and so, related to that, HOL being embedded in Isar would be part of
the game of embedding one language into another. If I find the right
pithy phrases, I can be perfectly content keeping my thoughts at a
high level, while allowing the backend prover to do its low-level magic.
Actually, an example of the "one language embedded into another game"
would be FOL embedded in HOL. In the process of building up HOL, you get
primitive type variables, the standard logical connectives and
quantifiers, the ability to define predicates, and the enforcement of
standard FOL formula-making rules. If you get rid of that part of HOL,
then you lose FOL too.
At some point, standard dictionary definitions don't completely
translate the meaning of formal, programming languages, on the other
hand, there's many times a strong relationship.
So, I'm deciding that I shouldn't confuse the "embedded game" with the
"framework game"; frameworks can be taken down, where embeddings
generally remain embedded.
I'm back to contemplating what may be involved with the Isar and HOL
"framework game", at least until I click the send button.
This archive was generated by a fusion of
Pipermail (Mailman edition) and