Generation of visitor components that implement program transformations

2001 ◽  
Vol 26 (3) ◽  
pp. 86-94
Author(s):  
R. E. Kurt Stirewalt ◽  
Laura K. Dillon
Keyword(s):  
Program Transformations

scholarly journals On the generalizability of Neural Program Models with respect to semantic-preserving program transformations

2021 ◽  
pp. 106552
Author(s):  
Md Rafiqul Islam Rabin ◽  
Nghi D.Q. Bui ◽  
Ke Wang ◽  
Yijun Yu ◽  
Lingxiao Jiang ◽  
...  
Keyword(s):  
Program Transformations

scholarly journals A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations

2008 ◽  
Vol 18 (3) ◽  
pp. 501-553 ◽  
Author(s):  
DAVID SABEL ◽  
MANFRED SCHMIDT-SCHAUSS
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Equational Theory ◽  
Order Reduction ◽  
Single Step ◽  
Program Transformations ◽  
Normal Order ◽  
Choice Context ◽  
Contextual Equivalence ◽  
Fairness Condition

We present a higher-order call-by-need lambda calculus enriched with constructors, case expressions, recursive letrec expressions, a seq operator for sequential evaluation and a non-deterministic operator amb that is locally bottom-avoiding. We use a small-step operational semantics in the form of a single-step rewriting system that defines a (non-deterministic) normal-order reduction. This strategy can be made fair by adding resources for book-keeping. As equational theory, we use contextual equivalence (that is, terms are equal if, when plugged into any program context, their termination behaviour is the same), in which we use a combination of may- and must-convergence, which is appropriate for non-deterministic computations. We show that we can drop the fairness condition for equational reasoning, since the valid equations with respect to normal-order reduction are the same as for fair normal-order reduction. We develop a number of proof tools for proving correctness of program transformations. In particular, we prove a context lemma for both may- and must- convergence that restricts the number of contexts that need to be examined for proving contextual equivalence. Combining this with so-called complete sets of commuting and forking diagrams, we show that all the deterministic reduction rules and some additional transformations preserve contextual equivalence. We also prove a standardisation theorem for fair normal-order reduction. The structure of the ordering ≤c is also analysed, and we show that Ω is not a least element and ≤c already implies contextual equivalence with respect to may-convergence.

Sign in / Sign up

Export Citation Format

Share Document