Re: [isabelle] check phases



On 30.07.2014 23:01, Makarius wrote:
> On Wed, 30 Jul 2014, Lars Noschinski wrote:
>
>> 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
>
> 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.
[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".



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