Abstract
We consider a class of languages of typed λ-expressions with first-order primitives and reflexive types and investigate which types it is useful and consistent to allow, when the meaning of a term is defined by its behaviour as a part of programs. We define the class of reducing types and show that it is irrelevant to allow the non-reducing ones in our languages. Moreover we prove that, for any language with reducing types and a sufficiently rich set of primitives there is a fully abstract model, in the sense of Milner.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E.Astesiano, G.Costa, On algebraic semantics of polyadic recursive schemas, 2me Coll. Les Arbres en Algèbre et en Programmation, Univ.of Lille, 1977, 29–83.
=== Fully abstract semantics for nondeterministic λ-s-calculi, 1979, to appear.
J.A. Goguen, J.W. Thatcher, E.G. Wagner, J.B. Wright, Initial algebra semantics and continuous algebras, JACM, 24 (1977) 68–95.
G. Berry, Séquentialité de l'évaluation formelle des λ-expressions, in B.Robinet ed. Trasformations des programmes (3me Coll. Int. sur la Programmation, Paris, 1978) Dunod, Paris 1978.
=== Stable models of typed λ-calculi, 5th ICALP, Udine 1978, Lecture Notes in C.S. 62, Springer, 72–89.
G.Berry, Modèles complètement adéquats et stables des λ-calculs typés, Thèse d'Etat, Univ. Paris VII, 1977.
C. Böhm, the CUCH as a formal and description language, in T.B. Steel ed. Formal language description languages for computer programming, North Holland, Amsterdam 1966, 179–197.
M.Coppo, M.Dezani-Ciancaglini, P.Sallé, Functional characterization of some semantic equalities inside λ-calculus, 6th ICALP, Graz 1979, Lecture Notes in C.S. 71, Springer.
B.Courcelle, G.Kahn, J.Vuillemin, Algorithmes d'équivalence et de réduction à des expressions minimales dans une classe d'équations récursives simples, Rapport IRIA n. 37, 1973.
E.Egli, Typed meanings in Scott's λ-calculus models, Symp. on λ-calculus and computer science theory, Rome 1975, Lecture Notes in C.S. 37, Springer.
E.Fehr, Lamda-calculus as control structures of programming languages, Report n.57, RWTH-Aachen, 1980.
H.F. Ledgard, Ten mini-languages: a study of topical issues in programming languages, Comp. Surv. 3 (1971) 115–146.
D.J.Lehmann, Modes in Algol Y, in Implementation and design of algoritmic languages, J.André, J.P.Banâtre eds. IRIA, 1977, 111–123.
J.J.Lévy, Reductions correctes et optimales dans le λ-calcul, Thèse d'Etat, Univ. Paris VII, 1978.
R.Milner, L.Morris, M.Newey, A logic for computable functions with reflexive and polymorphic types, in Proving and improving programs, G.Huet, G.Kahn eds. (Coll. IRIA, Arc et Senans, 1975), IRIA, 1975.
R. Milner, Processes, a mathematical model for computing agents, Studies in Logic 80, North Holland, 1975, 157–174.
===Fully abstract models of typed λ-calculi, TCS 4 (1977) 1–22.
G. Plotkin, LCF as a programming language, TCS 5 (1977) 223–255.
J.C.Reynolds, Notes on a lattice theoretic approach to the theory of computation, Syracuse University, 1972.
D.Scott, Data types as lattices, SIAM J. Comput. 5 (1976) n.3.
C.P. Wadsworth, The relation between computational and denotational properties of Scott's D∞ model of the λ-calculus, SIAM J. Comput. 5 (1976) 488–521.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1980 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Astesiano, E., Costa, G. (1980). Languages with reducing reflexive types. In: de Bakker, J., van Leeuwen, J. (eds) Automata, Languages and Programming. ICALP 1980. Lecture Notes in Computer Science, vol 85. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10003-2_58
Download citation
DOI: https://doi.org/10.1007/3-540-10003-2_58
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-10003-4
Online ISBN: 978-3-540-39346-7
eBook Packages: Springer Book Archive