Abstract
The constraint language for lambda structures (CLLS) can model lambda terms that are known only partially. In this paper, we introduce beta reduction constraints to describe beta reduction steps between partially known lambda terms. We show that beta reduction constraints can be expressed in an extension of CLLS by group parallelism. We then extend a known semi-decision procedure for CLLS to also deal with group parallelism and thus with beta-reduction constraints.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.
R. Backofen, J. Rogers, and K. Vijay-Shanker. A first-order axiomatization of the theory of finite trees. J. Logic, Language, and Information, 4(1):5–39, 1995.
M. Bodirsky, K. Erk, A. Koller, and J. Niehren. Beta reduction constraints, 2001. Full version. http://www.ps.uni-sb.de/Papers/abstracts/beta.html.
M. Bodirsky, K. Erk, A. Koller, and J. Niehren. Underspecified beta reduction, 2001. Submitted. http://www.ps.uni-sb.de/Papers/abstracts/usp-beta.html.
D. Duchier and J. Niehren. Dominance constraints with set operators. In First International Conference on Computational Logic (CL2000), LNCS, July 2000.
M. Egg, A. Koller, and J. Niehren. The Constraint Language for Lambda Structures. Journal of Logic, Language, and Information, 2001. To appear.
M. Egg, J. Niehren, P. Ruhrberg, and F. Xu. Constraints over lambda-structures in semantic underspecification. In In Proceedings COLING/ACL’98, 1998.
K. Erk, A. Koller, and J. Niehren. Processing underspecified semantic descriptions in CLLS. Journal of Language & Computation, 2001. To appear.
K. Erk and J. Niehren. Parallelism constraints. In Int. Conference on Rewriting Techniques and Applications, volume 1833 of LNCS, pages 110–126, 2000.
G. P. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.
J. Lamping. An algorithm for optimal lambda calculus reduction. In ACM Symposium on Principles of Programming Languages, pages 16–30, 1990.
J. Lévy. Linear second order unification. In 7th Int. Conference on Rewriting Techniques and Applications, volume 1103 of LNCS, pages 332–346, 1996.
M. P. Marcus, D. Hindle, and M. M. Fleck. D-theory: Talking about talking about trees. In Proceedings of the 21st ACL, pages 129–136, 1983.
M. Pinkal. Radical underspecification. In Proc. 10th Amsterdam Colloquium, 1996.
U. Reyle. Dealing with ambiguities by underspecification: construction, representation, and deduction. Journal of Semantics, 10:123–179, 1993.
M. Schmidt-Schauβ and K. Schulz. Solvability of context equations with two context variables is decidable. In Int. Conf. on Automated Deduction, LNCS, 1999.
K. van Deemter and S. Peters. Semantic Ambiguity and Underspecification. CSLI Press, Stanford, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodirsky, M., Erk, K., Koller, A., Niehren, J. (2001). Beta Reduction Constraints. In: Middeldorp, A. (eds) Rewriting Techniques and Applications. RTA 2001. Lecture Notes in Computer Science, vol 2051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45127-7_5
Download citation
DOI: https://doi.org/10.1007/3-540-45127-7_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42117-7
Online ISBN: 978-3-540-45127-3
eBook Packages: Springer Book Archive