Re: [isabelle] Encoding an evaluation context



On 21/04/06, Holger Gast <gast at informatik.uni-tuebingen.de> wrote:
> Michael Norrish discusses one solution (for HOL)
> in Section 3.3.1 (and various further spots for extensions):

> @PhdThesis{norrish98phd,
>   author =       {Norrish, Michael},
>   title =        {C formalised in {HOL}},
>   school =       {University of Cambridge},
>   year =         1998,
>   note =         {Technical Report UCAM-CL-TR-453}
> }

The approach I took ends up being pretty similar to the approach where
you have a context function that can span multiple levels of syntax,
but it does keep the recursion in just one place (the basic reduction
relation), rather than there, and also in the inductive
characterisation of what it is to be a valid context.

So you end up with a rule like

  e --> e'   validctxt c
-------------------------------
      c e --> c e'

as well as a definition of valid_ctxt that looks like

  valid_ctxt f == (\exists e2. f = \lambda e1. e1 + e2) \/
                       (\exists e1. f = \lambda e2. e1 + e2) \/
                       (f = unary_negation)

Michael





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