Computability of Phrases
- Predicate compH (computable):
- compintloc(p) := p
=>* v and v means l where l in Location is the meaning of p.
- compTexp(p) := p(s)
=>* v and v means n where s in Store and p(s) means n in [[T]].
- compcomm(p) := p(s)
=>* v and v means s' where s in Store and p(s) means s' in Store.
- compH[[U: H]]
holds for all well-typed phrases U: H.
- Induction on typing rules.
Computational adequacy follows from soundness of typing, soundness of
operational semantics and the computability of phrases.
Author: Wolfgang Schreiner
Last Modification: March 26, 1998