# Re: [isabelle] Embedded languages in Isabelle

• To: Daniel Kirchner <daniel at ekpyron.org>, cl-isabelle-users at lists.cam.ac.uk
• Subject: Re: [isabelle] Embedded languages in Isabelle
• From: Makarius <makarius at sketis.net>
• Date: Tue, 8 Oct 2019 14:00:50 +0200
• Authentication-results: mx2f26; spf=pass (sender IP is 62.216.204.180) smtp.mailfrom=makarius at sketis.net smtp.helo=[192.168.178.32]
• Autocrypt: addr=makarius at sketis.net; prefer-encrypt=mutual; keydata= mQINBFcrF+4BEADMcXMnu3XHg6bRsGe3tajAHqvm89+ecn/Y0WhjI2FplhkZs1LwM+ZA9eXh hiBrC/yX0FJ+qjzVIfm66CX4nzVG1f8qwaervMpvpA+gbhtQiXc0t+LDcqV+5cdtpKplPHSu oW+KzJKyCdkDB5fYMOzuaXQwYi12YAEQH2r6K7Q7Np+k82Xli1pWe+Tha/BH0pKJ5Q01aPep ASrNW9F+moX7C0fxWl65LiXGmF0UJep6fqKruhy8oNF4p6I2oZhktvaR/x6tkL2PkT3r+xUS 6g5i3BOjfwhoGY57nsioeK+8VFvdRH5DK4CbrTgDl7ddcrEeENrfpDiPLs/afVbe/T9oDXmJ OJAO4WMpfZNiFhx9SSVTHohw29Fyzn0N1UQGjPqAY1jg32DAxlnMQ0co/KabEFAcoQsW1/6U ZGiNxYVIyEKGrnSY4WuLuNC8CmU1RaYSdTk1y9tYdxufM9lH9ynzJwac6FdalOOxMR2G9JG8 L9/dk3ytlP6DVwkPBSCpJaTkTyMp1wSkF1oK/BDu5xKUQh0zvvLCuZ16hiKRBBSjpVExXRZC u+NC1Y4wqm1HOH7HBwgZ1Hv9S/EPmI9iwgcW0SpDJqPf2Cm7oFMZsZ5Dbs6/nOQoe4Zegy45 ymqDRlIekP7zj+vOoR80XAYfmAH5DElJHldcjmgLBMdpvvqGZwARAQABtB5NYWthcml1cyA8 bWFrYXJpdXNAc2tldGlzLm5ldD6JAj0EEwEIACcFAlcrF+4CGyMFCQlmAYAFCwkIBwIGFQgJ CgsCBBYCAwECHgECF4AACgkQ89KUEoG/TbiVrw/9FjEBgh2CB7Qof7Y4k0yc7j+x/A0Wmkc0 iwP5jaKJuxRv1JJT8CFqm392+/cdh3EkRUk/UWD+hpNndYJwxZltrEpKVqFAWoVOg3ZJ4cuI MYhlp4tk/T0KSl/gKT16dc6uJ7M/FzW0zv50vjFtAdianEDuqLXHKaGDUwWoOTDly0gdZ7aH /eNby6ONHUSJMdTNOErh2N+uESM4aZqUuuL/dTb6xiVzCpV5saT8EMakoazUd7QhoBaHvqfs BL7DEmvcTtA79GF3ufHrF/UndIcx8aMznZ2PGNjmy5seDCoKX0EYHdLam8vgo/TuU4dRw5Zn 6E/ouyNOliXT1Mn+SomeBSXTR5MXRq4TQ9MKVGiP0Yl+7GJQU0JFtDC1ZZEOyjIiwGWOhbUR pYujVm8C1iQ7NcEn2BqOAmRML6IR6+En4RLbgCNsBNXlmTPRJOaI+iV6DZzg3x9zcaDGhoYt jkBTEFpb0F3jU9yuaEU5401NV34fUxg8tqXs0R9CKinO7kQ8N+RDjyyY8k2KZiDYBJ6r+OK0 d7TaTj7F9tmpAu2pmQ8lxOKjDZIwlbGTsC4lxISmcPzBGTKXja5nakcWYx/lZ4vje0WZ12HN amnD1weakFixRYit0d+Kz7cuj684NSbhwC0oN2t9R06Nfq8UPEWRKEitCly0OtRgio8zVZ/L eAC5Ag0EVysX7gEQAKs5NVOvYkE/r8KLsJ8/L/9eulpJDOFilZ9fyuqii7t1UpHZLb58QghW JM+IB2GSGsB+pOi6Je7hmwxcVdXYbGlYZ4Btqqw48/XptfbNZ8alCk6AqoVFP4MbYxij/Qqv f/Yw6GR0p1RIC/W4GF/JgDDwDFEiMT6Pv6dpM8acdNFCERDZdoOJiC+XJRwy5lZ2g5FOJkT9 rVI9EnA7mBXLLjPOMUp2/eZxN6gKOZzI3ej9vixg3adWR2yfKPgacHP/ujnVfITOl0OyLE5f zIHq85dEV4zW6Mpx7+Um0tdkwlUVMaW2nQ1bcwejgVAuD/MLSF/lSs3N5D1ctw5QUemYh7/e 2dC12UJuFDFxNPzcltQTlkBCVWV1D0SjScDHdlF6HhzpZOlt52/rwTn5GHtY4nwAL4IJ+Yvl WX8YKmyILH4Ai8c/N2IVRERQ2qorWFlsQnqrXV+hXf8aUwjc/pq4K9rsWxvle3TpeZfoBefU /s1PEX0SepZFAqAXHlQ9DZPsdPDo9EFK695G5w4nf03EhE9TV1MKGUuc1XJ6f1ZLaxu0TwTA 6qYtKIyBcU0Yn61S2Kh7Dgb5LdLV8nfl71+n/xIt2IWH5UJ9YuwEgGEP0c6ImnAUZ+nRodFI 0RwtCWlRkSJWtQln1vcphrz8PjWZH6e/nWnceXR/Al5P0WexQgtvABEBAAGJAiUEGAEIAA8F AlcrF+4CGwwFCQlmAYAACgkQ89KUEoG/Tbh7VQ/9Fc4bdwJYc3jH/LiuXv6uMg50Cv6lg2NT bL9DClWGNiYzejfM2A4c5K+GRUXhyD7S9U203MOv3z7uTbtyQL8XVolNnQlRIkB00f8nJ2sw HMXx/hemjXBvtlneq+vrMORJexldXUMFq19ZZrvj0zZL+pUnGFqt+IWTEE5GpL7wu20Demaj jYyGyKcDZyJOWZcl4e45Yn3hl0EI2xVmVh7ZinVsb3+nqgcltFy4Jt+drezwV2EiLGJHfGsT jEQb3C9VpneU4Jo+hHtfqLK4Q8+WlIOzSfyvwbabxrhyqg7i11fu8yckNW3dCURPYigV07HK 4dN0zhj53M0Q3eTwegJRPJb8XoLDcSdbsaU2HIShlGDKmzS9KL4JzLikQ9dXROC4cae3jRKH aexFi4B55Ab6FxIfXj09wUCO6Nm0owDfIBDMgiywvi2Rb2etCjBgRbSj71S2nntd9ZitoYvE yKirLkWmJRbp3ln8cHi8Uc/jr1cDPVRWuLUN0uceMj5+AR+NZVakcNUHWJCinMMjacho0SyP QmocdU8pzzupreaVWruqaSzqcpWBPwrE5OxEtJ+OyIBjKmRJ5eptjh4rKgNaVnKjhqbvr+Yz pUAgPp38jjf4HJghUGIfWArKNelKJEJOYk94DAbmT67LgqEdZ0yaA2BCHmreN727WIzV9vkX NMc=
• Openpgp: preference=signencrypt
• References: <2074102.1x7EFbrfS5@ekpyrosis> <417e9726-7ca2-f1c9-3a45-14ed9ee293a7@sketis.net> <b2cde4fd-06c9-383a-184f-145822b200ce@sketis.net> <1814985.lC9oWjBFk6@ekpyrosis>
• User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.8.0

On 03/10/2019 17:29, Daniel Kirchner wrote:
>
> To say a bit more about my application: I'm constructing a shallow semantic
> embedding of a philosophical logic (Edward Zalta's "Theory of Abstract
> Objects"). That logic is quite different from HOL in multiple ways, which makes
> this an interesting research project. For example the language contains two
> kinds of atomic formulas, i.e. Fxy "x and y 'exemplify' F" and xyF "x and y
> 'encode' F", neither of which can be implemented as mere function application
> in an embedding in HOL. The variable names have type implications, e.g. x and
> y have a different type than F and G, which again have a different type from
> e.g. \kappa, etc. - some of these types map directly to types in HOL, others I
> need to implement with guarding behind additional constants, etc.

Thanks for the general application outline -- it is always important to
keep the big picture in mind. A language that is very different from the
Isabelle/Pure lambda calculus (which is reused in the Isabelle/HOL
library) definitely poses a challenge. It will require very careful
exploration to do just the right thing, otherwise it will lead to an
unmaintainable blob of "code" that nobody can understand nor maintain.

> The target logic itself also defines new symbols in terms of its basic symbols,
> so the implementation should be extensible very much like with mixfix
> annotations to constants or "syntax" commands. That's why I'm trying to avoid
> duplicating an implementation of a priority grammar. (The definitions in the
> target logic themselves are not quite the same as Isar definitions, so I will
> probably introduce new outer syntax commands for them, but in the end they
> will translate to "plain", but more complex definitions satisfying the narrowly
> defined inferential role of definitions in the hyper-intensional free logic of
> the target system).

Note that there are different levels of complexity rolled into Isabelle
term notation. A command like 'notation' with plain mixfix is relatively
close to the priority grammer: if you subtract special things like
'binder' from the mixfix syntax, it is even simpler. In contrast,
'syntax' + 'translations' (or 'parse_translation' etc.) opens a not so
does not require that, it would greatly simplify a standalone
implementation of it (one that is independent of the Isabelle "syntax
phases").

> At the moment I'm trying to only *parse* the actual syntax of the language,
> not to print it, i.e. a formula given in the syntax of the target logic, will
> be translated to its representation in Isabelle's term logic and further
> reasoning will be done in Isabelle's term logic directly (I think this should
> alleviate the problem of transformed names like x_ and xa, but at a later
> stage it might also be interesting to go further and print in the target
> logic's syntax and continue reasoning in it as well, for which this indeed
> will be an issue).

BTW, printing also means document output of the sources in HTML or
LaTeX. There is an implicit assumption that adjacent letters for one
word, not individual identifiers. Compare this with LaTeX typesetting of
$abc$ vs. \emph{abc}. Presently, there is no proper way in the document
preparation system to change the typesetting of names, but it is
conceivable that a future notion of antiquotations within terms could
also go through document presentation.

> I'm now trying to mainly stay within the Isabelle term language itself.
> Interestingly, only now after looking through the syntax parsing ML code I
> realize that I can do much more than I thought within its boundaries.
>
> Simplified that approach will look like
>
> consts valid :: "p => bool"
> consts emb_implies :: "p => p => p"
> nonterminal q
> syntax valid :: "q => bool" ("[\Turnstile _]")
>              emb_implies "q => q => q" (infixl "->" 8)
>              emb_not "q => q" ("\<not>_" [40] 70)
>              "_atomic_formula" :: "id_position => q" ("_")
> etc.
>
> and then installing a parse_ast_translation for "_atomic_formula" which splits
> up e.g. "Fxy" to "(_exe F x y)" and "xyF" to "(_enc x y F)", which is then
> translated to the corresponding term in a parse_translation.

This looks much better to me. It deescalates the overall complexity of
the implementation by some orders of magnitude.

Apart from id_position you can also experiment with cartouches for
certain well-defined sub-languages.

> In general in the long run it would, of course, be nice to have a self-
> contained "reentrant" and "public" version of the parser for Isabelle's term
> language in ML, in which every aspect could be customized, including the
> lexicon and tokenizing and maybe even the generation of "fresh" variable
> names, etc. - but I realize that this is way too much to ask especially for my
> very specific and probably rather exotic use case :-).

This sounds a bit like marketing talk for "software frameworks". Such
software components don't exist, and where people have tried it its has

The inner syntax implementation of Isabelle/Pure is the opposite of
that. It has many special tricks based on the particular situation to
make it just work by accident. I have reworked the architecture and
implementation many times in the past 25 years. A few more reforms of it
are still in the pipeline, e.g. subterm PIDE markup as seen in the tiny
rail example.

Such reforms naturally break bad applications of it -- or the other way
round: bad applications prevent further reforms.

Makarius



Attachment: signature.asc
Description: OpenPGP digital signature

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