No-function-definitions-in-dynamic-semantics
The condition in which function definitions are elsewhere,
applied to entities in the dynamic semntics.
We extend the ...-nofunp predicates
defined in no-function-definitions
to some of the dynamic semantics entities.
This extension serves to take advantage of this condition
in proofs of dynamic correctness of transformations
that assume that the code satisfies the condition.
In fact, we prove theorems that are used in such proofs.
Subtopics
- Funinfo+funenv-nofunp
- Check that
a pair consisting of function information and a function environment
has no function definitions in the functions' bodies.
- Funscope-nofunp
- Check that a function scope
has no function definitions in the functions' bodies.
- Funinfo-nofunp
- Check that a function information
has no function definitions in the function's body.
- Funenv-nofunp
- Check that a function environment
has no function definitions in the functions' bodies.
- Funenv-nofunp-of-add-funs
- Theorem about add-funs and ...-nofunp.
- Funinfo+funenv-nofunp-of-find-fun
- Theorem about find-fun and ...-nofunp.
