Email Gateway (Aug 17 2022 at 14:16): Email Gateway (Aug 17 2022 at 14:16):From: Klaus Ostermann <ostermann@informatik.tu-darmstadt.de>
Hi there,
I am trying to formalize a programming language semantics.
Small-step semantics are frequently formalized by using an evaluation
context which controls the order of evaluation.
What would be a good way to encode an evaluation context in Isabelle? Are
there maybe existing examples that I could look at?
Regards,
Klaus
Email Gateway (Aug 17 2022 at 14:16):From: nipkow@in.tum.de
Alternatively you can encode the evaluation contexts as congruence rules: for
each pattern in the context grammar you define a rule
xi -> xi'
c x1 ... xn -> c x1 .. xi' xn
This is very straightforward but does not please friends of eval-contexts.
Tobias
Email Gateway (Aug 17 2022 at 14:16):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Hallo Klaus,
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}
}
Email Gateway (Aug 17 2022 at 14:16):From: Norbert Schirmer <norbert.schirmer@web.de>
Hello Klaus
See for example the work of Stefan Berghofer for the Poplmark-Challenge:
http://www4.in.tum.de/~berghofe/papers/Poplmark/index.html
He uses a function E:: term => term to encode evalution contexts.
An inductive definition "ctxt" restricts the E to sensible functions.
Norbert
Email Gateway (Aug 17 2022 at 14:16):From: Michael Norrish <michael.norrish@gmail.com>
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
Last updated: May 03 2024 at 12:27 UTC