Email Gateway (Aug 18 2022 at 16:51): Email Gateway (Aug 18 2022 at 16:51):From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Is this some standard notion of Event-B explained in the literature
somewhere?
Yes and no. It is some standard Event-B notation (set comprehension) but
I am not aware of an explanation in the literature. I have thus written
my own specification documentation:
ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/698.pdf
Avoiding auxiliary notation, the Event-B set comprehension
"{x y. phi x y .| t x y}"
stands for
"(if
\<forall> phi x y.
phi x y \<noteq> None \<and> (the (phi x y) --> t x y \<noteq> None)
then Some {the (t x y) | x y. the (phi x y)}
else None)"
You then provide ML 'parse_translation' and 'print_translation' in the
known manner. Moreover, the inner check/uncheck phase is configured
like this:declaration {* K (Syntax.add_term_check 0 "my_check" my_check) *}
Here my_check is your function to operate on simultatenously on a given
input or output situation (consiting of terms). It returns either SOME
changed result, or NONE for identity. See also e.g. see
src/Pure/Isar/proof_context.ML how expand_abbrevs and contract_abbrevs
are done. This is really a user-space mechanism.
I think this is the missing piece of the puzzle. I have been unaware
that I can install transformations after type checking.
Thanks,
Matthias
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iD8DBQFNQFuwczhznXSdWggRAhRmAJ9XkaiVKy2RkFHSm7eYLGrzFCmyOACfWgbC
ETux71Xyh2E/whWf0IQgd48=
=KMHG
-----END PGP SIGNATURE-----
Email Gateway (Aug 18 2022 at 16:56):From: Makarius <makarius@sketis.net>
Not really, at least not at the raw parse tree level. Duplication of
subtrees as above (and likewise comparison of subtrees for printing) looks
suspicious.
Nonetheless, it should work by separating the concrete from the abstract
syntax. I.e. "foo" is like a regular binder, and there is an abbreviation
for the rest. Abbreviations work by higher-order rewriting on fully-typed
lambda terms.
Makarius
Email Gateway (Aug 18 2022 at 16:56):From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Makarius schrieb:
On Fri, 14 Jan 2011, Matthias Schmalz wrote:
- Consider the following contrieved parse translation translating
"foo x. t" to "(\<forall> x. t) \<and> (\<forall> x. t)":term "foo x. True"
(with show_types activated) I get
"(\<forall> x::'a. True) \<and> (\<forall> x::'b. True)".
(The two occurrences of x have different types.)Is it possible to change the parse translation so that
term "foo x. True"
yields "(\<forall> x::'a. True) \<and> (\<forall> x::'a. True)".
(The two occurrences of x have the same type.)Not really, at least not at the raw parse tree level. Duplication of
subtrees as above (and likewise comparison of subtrees for printing)
looks suspicious.
That is good to know. So I will stop trying.
Nonetheless, it should work by separating the concrete from the abstract
syntax. I.e. "foo" is like a regular binder, and there is an
abbreviation for the rest. Abbreviations work by higher-order rewriting
on fully-typed lambda terms.
The binder(s) I actually want to define has the following characteristics:
no simple recursive definition (like set comprehension, unlike
\<forall>, as \<forall> x xs. p == \<forall> x. \<forall> xs. p)
the right-hand side of the definition has an extra bound variable
(like set comprehension:
{t | xs. p} == {y. \<exists> xs. y = t \<and> p})
the right-hand side binds the bound variables of the left-hand side
several times such as in:
foo xs. p == (\<forall> xs. p) \<and> (\<exists> xs. p)
The multiple bound variables make it hard to work with abbreviations.
I will try to cook something up with overloading (to cope with the
arbitrary number of bound variables). If that does not work out, I will
define (on demand) several constants foo1, foo2, ..., one for each
number of bound variables.
Maybe somebody on the list can point to a running example of a binder
with the above properties? That would be helpful.
Anyway, thanks for the explanations,
Matthias
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iD8DBQFNMyPfczhznXSdWggRAlcOAJ99BjR5aGRtjitF4CoPNY4bvIv5eQCeLZoe
/D5T7dSFzOeQlzXAEuswYxc=
=2xd+
-----END PGP SIGNATURE-----
Email Gateway (Aug 18 2022 at 17:01):From: Makarius <makarius@sketis.net>
Is this some standard notion of Event-B explained in the literature
somewhere?
Anyway, the aforementioned idea of separating the concrete syntax (with
the binding) from the abstract syntax (with the duplication of subterms)
works along these lines:
abbreviation Foo :: "('a => bool) => bool" (binder "FOO " 10)
where "Foo b == (ALL x. b x) & (EX x. b x)"
There are two syntax layers involved here: the "binder" annotation
produces some standard parse/print translation for iterated binders; the
rewrite rule operates on fully type-checked lambda terms -- when the
regular type-inference is already finished.
At both layers you can install your own ML function to operate on parse
terms and typed lambda terms, respectively. You merely declare an
uninterpreted constant like this:
axiomatization Foo :: "('a => bool) => bool"
or any other type scheme that fits for your application. Note that
'axiomatization' instead of 'consts' ensures that the user cannot
accidentally define Foo later on.
You then provide ML 'parse_translation' and 'print_translation' in the
known manner. Moreover, the inner check/uncheck phase is configured like
this:
declaration {* K (Syntax.add_term_check 0 "my_check" my_check) *}
Here my_check is your function to operate on simultatenously on a given
input or output situation (consiting of terms). It returns either SOME
changed result, or NONE for identity. See also e.g. see
src/Pure/Isar/proof_context.ML how expand_abbrevs and contract_abbrevs are
done. This is really a user-space mechanism.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC