Perpetual Reductions inλ-Calculus
F van Raamsdonk, P Severi, MHB Sørensen… - Information and …, 1999 - Elsevier
This paper surveys a part of the theory ofβ-reduction inλ-calculus which might aptly be
calledperpetual reductions. The theory is concerned withperpetual reduction strategies, ie …
calledperpetual reductions. The theory is concerned withperpetual reduction strategies, ie …
Call by need computations to root-stable form
A Middeldorp - Proceedings of the 24th ACM SIGPLAN-SIGACT …, 1997 - dl.acm.org
The following theorem of Huet and Lévy forms the basis of all results on optimal reduction
strategies for orthogonal term rewriting systems: every term not in normal form contains a …
strategies for orthogonal term rewriting systems: every term not in normal form contains a …
Descendants and origins in term rewriting
In this paper we treat various aspects of a notion that is central in term rewriting, namely that
of descendants or residuals. We address both first-order term rewriting and λ-calculus, their …
of descendants or residuals. We address both first-order term rewriting and λ-calculus, their …
Relative normalization in deterministic residual structures
J Glauert, Z Khasidashvili - Colloquium on Trees in Algebra and …, 1996 - Springer
This paper generalizes the Huet and Lévy theory of normalization by neededness to an
abstract setting. We define Stable Deterministic Residual Structures (SDRS) and …
abstract setting. We define Stable Deterministic Residual Structures (SDRS) and …
Weak optimality, and the meaning of sharing
T Balabonski - ACM SIGPLAN Notices, 2013 - dl.acm.org
In this paper we investigate laziness and optimal evaluation strategies for functional
programming languages. We consider the weak lambda-calculus as a basis of functional …
programming languages. We consider the weak lambda-calculus as a basis of functional …
Discrete normalization and standardization in deterministic residual structures
Z Khasidashvili, J Glauert - International Conference on Algebraic and …, 1996 - Springer
We prove a version of the Standardization Theorem and the Discrete Normalization
Theorem in stable Deterministic Residual Structures, Abstract Reduction Systems with …
Theorem in stable Deterministic Residual Structures, Abstract Reduction Systems with …
Relative normalization in orthogonal expression reduction systems
J Glauert, Z Khasidashvili - International Workshop on Conditional Term …, 1994 - Springer
We study reductions in orthogonal (left-linear and non-ambiguous) Expression Reduction
Systems, a formalism for Term Rewriting Systems with bound variables and substitutions. To …
Systems, a formalism for Term Rewriting Systems with bound variables and substitutions. To …
Ground reducibility and automata with disequality constraints
H Comon, F Jacquemard - Annual Symposium on Theoretical Aspects of …, 1994 - Springer
Ground reducibility and automata with disequality constraints Page 1 Term Rewriting and
Unification Page 2 Page 3 Ground Reducibility and Automata with Disequality Constraints …
Unification Page 2 Page 3 Ground Reducibility and Automata with Disequality Constraints …
The longest perpetual reductions in orthogonal expression reduction systems
Z Khasidashvili - International Symposium on Logical Foundations of …, 1994 - Springer
We consider reductions in Orthogonal Expression Reduction Systems (OERS), that is,
Orthogonal Term Rewriting Systems with bound variables and substitutions, as in the λ …
Orthogonal Term Rewriting Systems with bound variables and substitutions, as in the λ …
On higher order recursive program schemes
Z Khasidashvili - Colloquium on Trees in Algebra and Programming, 1994 - Springer
Abstract We define Higher Order Recursive Program Schemes (HRPSs) by allowing
metasubstitutions (as in the λ-calculus) in right-hand sides of function and quantifier …
metasubstitutions (as in the λ-calculus) in right-hand sides of function and quantifier …