Email Gateway (Aug 19 2022 at 15:08): Email Gateway (Aug 19 2022 at 15:08):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
what transformations are allowed for check phases and which invariants
can I expect to be preserved by check phases? I couldn't find anything
in the implementation manual, but the reference manual at least states
(section 7.5):
Pre-terms are further processed by the so-called check and uncheck
phases that are intertwined with type-inference (see also [49]). The
latter allows to operate on higher-order abstract syntax with proper
binding an type information already available
(although I'm not sure what "latter" refers to here).
The invariant I am interested in is the preservation of binders: Given a
constant c (declared by myself, so no check-phase should know about it)
and an (unchecked) term t containing c exactly once, then the
Abs(tractions) in t above c are the same as the abstractions above c in
Syntax.check_term ctxt t (of course "same" is a bit fuzzy here --
obviously types and names might change).
Is this a reasonable expectation?
Email Gateway (Aug 19 2022 at 15:09):From: Lars Noschinski <noschinl@in.tum.de>
To provide a bit of background: The pat_subst tool we presented at the
Isabelle workshop allows pattern of the form
at "Suc x" in "{x. _ + HOLE}"
to describe for example the subterm "Suc y" in the term "{y. 1 + (Suc y
I achieve that by parsing the terms separatly and calling
Syntax.check_terms on
["Suc x", "x :: '?a", "{x :: '?a. _ + HOLE}"
(where ":: '?a" are type constraints added with Type.constraint). Now,
after checking the terms, I need to be able to associate the free
variables which the right bound variables again. If I can expect the
bound variables between root and HOLE to be the same before and after
the check, this is easy.
-- Lars
Email Gateway (Aug 19 2022 at 15:09):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
I don't know if this will help with your application, but "Term.rename_abs" might be part of the solution.
Jasmin
Email Gateway (Aug 19 2022 at 15:10):From: Makarius <makarius@sketis.net>
See chapter 3 of the "implementation" manual. For Isabelle2014 I have
extended and refined this again (last June).
If there is anything important missing or unclear, we can discuss that,
especially for the coming release.
Makarius
Email Gateway (Aug 19 2022 at 15:42):From: Lars Noschinski <noschinl@in.tum.de>
[Everything here refers to 2014-RC1]
On the topic of seperation of parse and check, the manual states:
Note that the formal status of bound variables, versus free
variables, versus constants must not be changed between these phases.
And
The check phase is meant to subsume a variety of mechanisms in the
manner of "type-inference" or "type-reconstruction" or
"type-improvement", not just type-checking in the narrow sense.
By the latter sentence, modifying types and type constraints is
obviously in the scope of check. I'd interpret the former as "a check
module transforms bounds to bounds, frees to frees and constants to
constants". However, the abbreviation mechanism is allowed to replace
subterms (with a certain constant at the root) by (almost) arbitrary
other subterms (but without capturing additional variables).
Similarly (but not mentioned), the "_" will be replaced by a Var,
capturing all available bounds. So I guess, the first quoted sentence
needs to be read as
Bounds stay bounds, Frees stay Frees, subterms starting with Consts
can be transformed almost arbitrarily (although they are probably
not allowed to introduce new, previously unfixed, frees).
The manual doesn't mention abstractions, so I assume that there are
cases where eta-contraction or even beta-reduction would be deemed as
allowed steps for a check module.
BTW, a small nitpick: In the last sentence in the paragraph on
Syntax.read_terms (bottom of page 93), the reference to §3.3 is missing
parentheses or a "see".
Email Gateway (Aug 19 2022 at 15:42):From: Makarius <makarius@sketis.net>
On Fri, 1 Aug 2014, Lars Noschinski wrote:
And
The check phase is meant to subsume a variety of mechanisms in the
manner of "type-inference" or "type-reconstruction" or
"type-improvement", not just type-checking in the narrow sense.By the latter sentence, modifying types and type constraints is
obviously in the scope of check.
Yes, type constraints and certain change of status of type variables is
possible, and actually the main purpose of certain check phases. The
implementation manual has some general explanations on the implicit
polymorphism of terms that apply here as well.
In other situations, term checks perform some kind of higher-order
rewriting. This might include alpha-beta-eta conversions, although within
the syntax one needs to be more careful than within the logic, to avoid
too much user-confusion. Tool confusion is a different thing: in full
generality, the mix of check phases might not work out at all.
Similarly (but not mentioned), the "_" will be replaced by a Var,
capturing all available bounds.
That is some special trickery with "dummy_pattern" -- probably not
something to try at home.
Makarius
Email Gateway (Aug 19 2022 at 15:42):From: Makarius <makarius@sketis.net>
Reading this description twice, I would say it should work, but there
might be fine points to be observed.
I still need to read your paper from the Isabelle workshop -- it is
already printed out and on the top of the stack.
Makarius
Last updated: Apr 19 2024 at 12:27 UTC