Abstract:
In this article, we address the problem of expansion with respect to rules of a calculus with explicit substitution. Mainly, we analyse the λυ- and λs-calculi sets of terms having the property of expansion to pure terms, as minimal sets of terms for these calculi. We prove that, contrarily to what happens in the λx-calculus in which this set is trivial, for λυ and λs they are proper and non-recursive, so a calculus based on a minimal set of terms has a syntax which is not context-free and hence cannot be presented in the usual way. © The Author, 2008. Published by Oxford University Press. All rights reserved.
Registro:
Documento: |
Artículo
|
Título: | The expansion problem in lambda calculi with explicit substitution |
Autor: | Arbiser, A. |
Filiación: | Department of Computer Science, University of Buenos Aires, Ciudad Universitaria, (1428) Buenos Aires, Argentina
|
Palabras clave: | Context-free; Expansion; Explicit substitution; Lambda calculus; Lambda upsilon; Lambda's; Recursiv set; Biomineralization; Differentiation (calculus); Pathology; Context-free; Explicit substitution; Lambda calculus; Lambda upsilon; Lambda's; Recursiv set; Calculations |
Año: | 2008
|
Volumen: | 18
|
Número: | 6
|
Página de inicio: | 849
|
Página de fin: | 883
|
DOI: |
http://dx.doi.org/10.1093/logcom/exn007 |
Título revista: | Journal of Logic and Computation
|
Título revista abreviado: | J Logic Comput
|
ISSN: | 0955792X
|
CODEN: | JLCOE
|
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v18_n6_p849_Arbiser |
Referencias:
- Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J., Explicit substitutions (1991) Journal of Functional Programming, 1, pp. 375-416
- A. Arbiser, E. Bonelli, and A. Ríos. Perpetuality in a lambda calculus with explicit substitution and composition. In Proceedings of the WAIT 2002, 31 JAIIO. S ADIO (Sociedad Argentina de Informática e Investigación Operativa), Santa Fe, 2002; Arbiser, A., (2005) Explicit Substitution Systems and Subsystems, , PhD Thesis, University of Buenos Aires
- H. P. Barendregt. The Lambda Calculus: its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, revised edition, 1984; Barendregt, H.P., Lambda calculi with types (1992) Handbook of Logic in Computer Science, 2, pp. 117-309. , S. Abramsky, D. Gabbay, and T. S. E. Maibaum eds, ch. 2, pp, Oxford University Press, Oxford
- Bloo, R., (1997) Preservation of Termination for Explicit Substitutions, , PhD thesis, Eindhoven University
- de Bruijn, N., Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem (1972) Indagations Mathematicae, 34, pp. 381-392
- Church, A., Rosser, J.B., Some Properties of Conversion (1936) Transactions of the American Mathematical Society, 39, pp. 472-482
- Davis, M., Weyuker, E., (1994) Computability, Complexity and Languages: Fundamentals of Theoretical, , Computer Science. Academic Press, New York
- Kamareddine, F., Ríbs, A., A λ-calculus à la de Bruijn with explicit substitutions (1995) Lecture Notes in Computer Science, 982, pp. 45-62. , Proceedings of PLILP'95
- Herbelin, H., Expicit substitutions and reducibility (2001) Journal of Logic and Computation, 11, pp. 429-449
- Kamareddine, F., Ríos, A., Relating the λσ- and λs-styles of explicit substitutions (2000) Journal of Logic and Computation, 10, pp. 349-380
- Lescanne, P., Rouyer-Degli, J., Benaissa, Z., Briaud, D., Lambda-upsilon, a calculus of explicit substitutions which preserves strong normalisation (1996) Journal of Functional Programming, 6, pp. 699-722
- Polonovski, E., (2004) Substitutions Explicites, Logique et Normalisation, , PhD Thesis, Université de Paris VII
- K. H. Rose. Explicit cyclic substitutions. In Proceedings CTRS '92 - 3rd International Workshop on Conditional Term Rewriting Systems, Lecture Notes in Computer Science 656, M. Rusinowitch and J.-L. Rémy, eds, pp. 36-50, Pont-a-Mousson, France, Springer-Verlag, 1992; van Raamsdonk, F., Severi, P., Sørensen, M.H., Xi, H., Perpetual reductions in lambda calculus (1999) Journal of Information and Computation, 149, pp. 173-225
- Waldmann, J., (1998) The Combinator S, , PhD thesis, Friedrich-Schiller- Universität Jena
Citas:
---------- APA ----------
(2008)
. The expansion problem in lambda calculi with explicit substitution. Journal of Logic and Computation, 18(6), 849-883.
http://dx.doi.org/10.1093/logcom/exn007---------- CHICAGO ----------
Arbiser, A.
"The expansion problem in lambda calculi with explicit substitution"
. Journal of Logic and Computation 18, no. 6
(2008) : 849-883.
http://dx.doi.org/10.1093/logcom/exn007---------- MLA ----------
Arbiser, A.
"The expansion problem in lambda calculi with explicit substitution"
. Journal of Logic and Computation, vol. 18, no. 6, 2008, pp. 849-883.
http://dx.doi.org/10.1093/logcom/exn007---------- VANCOUVER ----------
Arbiser, A. The expansion problem in lambda calculi with explicit substitution. J Logic Comput. 2008;18(6):849-883.
http://dx.doi.org/10.1093/logcom/exn007