Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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