Email Gateway (Aug 22 2022 at 20:24): Email Gateway (Aug 22 2022 at 20:24):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
Dear Isabelle Users,
I'm currently working on a project where I want to have polymorphic "fixes"
constants in locales. The context is that I'm trying to build a framework
for composing semantics of certain types of syntax trees with extension
points represented as Isabelle type variables. My goal is to achieve a
separation of concerns between pieces of the semantics that only care about
the structure of the tree, and other that only care about the concrete data
embedded at individual nodes in the tree. For the former, I want something
like
(* 1 *) "(forall 't1 't2 't3 . 'x => ('t1, 't2, 't3) gensyn => 'mstate =>
'mstate)"
(Gensyn being the name of the syntax tree data structure). I'd like to use
locales to declare semantics for different specialized types of this syntax
tree. Each locale will have parameters that look like the above. These
parameters are integrated together to give a semantics that has a type like
the following:
(* 2 *) "('x, 'y, 'z) syntax => 'state => 'state"
The definition of this semantics (as an inductive) happens inside a locale
with equation (1) as a fixes parameter. Note that is should be invalid
for Isabelle
to assume that it is always the case that 't1 = 'x, 't2 = 'y, 't3 = 'z,
etc. This would make the parameter "not parametric enough", and allow the
user to pass in terms that "know too much" about the data stored at nodes
in the tree.
My (handwavey) understanding of how polymorphism works in Isabelle is that
only "finished" definitions are allowed to be let-polymorphic, and "fixes"
in locales aren't "finished" in the appropriate way. It seems that in
proof-contexts there is a "let" command that could be used that might be
helpful here, but locales don't seem to have an equivalent.
I've looked into using Isabelle's Overloading facility, but this doesn't
achieve exactly what I want, because there doesn't seem to be any way to do
Overloading inside of a local context, and I may want to declare multiple
different semantics for different syntax trees of the same (specialized)
type (I'd like to be able to isolate each one into its own locale).
Typeclasses have the same problem: I want to be able to define possibly
different implementations for the same type, and let the user select them
by choosing the appropriate locale.
Are there any other options I have? I've attached a stripped-down version
of what I'm trying to implement; hopefully it won't be too difficult to see
where this problem arises (note that I am using Isabelle2018 rather than
Isabelle2019, although I imagine that Isabelle2019 would give the same
result).
Best,
Mario
ParamExample.thy
Last updated: Nov 21 2024 at 12:39 UTC