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 MHonArc.