Defining Recursors by Solving Equations in Second-Order Lambda Calculus

• Autorzy: Spławski Z.
• Języki publikacji: PL

Abstrakty

EN

Positive recursive (fixpoint) types can be added to the polymorphic (Church-style) lambda calculus l2 (System F) in several different ways, depending on the choice of the elimination operator. Known extensions of l2 fall into two equivalence classes with respect to mutual interpretability by means of beta-eta reductions, and elimination operators for fixpoint types can be classified accordingly as either "iterators" or "recursors". Systems with iterators can be defined within l2 by means of beta reductions, and it is conjectured that systems with recursors cannot. In this paper we define the general form of mutual iteration scheme in l2 and we show that the explicit solution for particular functions defines recursors within l2, though proof of this fact requires much more than beta reductions, namely parametricity. We propose a convenient equational inference rule which can be used instead of parametricity for proving equational properties of polymorphic functions, defined by iterators.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Schedae Informaticae
• Rocznik: 2003
• Tom: Vol. 12
• Strony: 49--56
• Opis fizyczny: Bibliogr. 11 poz.

Twórcy

autor

Spławski Z.

• Faculty of Informatics and Management University of Technology, Wybrzeże Wyspiańskiego 27, 50-370 Wrocław, Poland,

Bibliografia

• [1] Böhm C., Berarducci A.; Automatic synthesis of typed Λ-programs on term algebras, Theoretical Computer Science, Vol. 39(2/3), 1985, pp. 135–154.
• [2] Böhm C.; Reducing Recursion to Iteration by Means of Pairs and N-tuples, in: M. Boscarol et al., (eds.), Foundations of Logic and Functional Programming, Lecture Notes in Computer Science, Vol. 306, Springer–Verlag, Berlin 1988, pp. 58–66.
• [3] Girard J.-Y.; Une extension de l’interpretation de Gödel á lánalyse, et son application á l’elimination de coupures dans l’analyse et la theorie des types, in: J.E. Fenstad, (ed.), Proceedings of the Second Scandinavian Logic Symposium,North-Holland, Amsterdam 1971, pp. 63–92.
• [4] Girard J.-Y., Lafont Y., Taylor P.; Proofs and Types, Cambridge University Press, Cambridge 1990.
• [5] Krivine J.-L., Parigot M.; Programming with proofs, Journal of Information Processing and Cybernetics, 26(3), 1990, pp. 149–167.
• [6] Mendler N.P.; Recursive types and type constraints in the second-order lambda calculus, in: Proc. 2nd Symposium on Logic in Computer Science, IEEE, 1987, pp. 30–36.
• [7] Mendler N.P.; Inductive types and type constraints in the second-order lambda calculus, Annals of Pure and Applied Logic, 51(1/2), 1991, pp. 159–172.
• [8] Plotkin G., Abadi M.; A Logic for Parametric Polymorphism, in: M. Bezem, J.F. Groote, (eds.), Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, Vol. 664, Springer–Verlag, Berlin 1993, pp. 361–375.
• [9] Reynolds J.C.; Towards a theory of type structure, in: B. Robinet, (ed.), Colloque sur la Programmation, Lecture Notes in Computer Science, Vol. 19, Springer–Verlag, 1974, pp. 408–425.
• [10] Reynolds J.C.; Types, Abstraction and Parametric Polymorphism, in: R.E.A. Mason, (ed.), Information Processing 83, North-Holland, Amsterdam 1983, pp. 513–523.
• [11] Spławski Z., Urzyczyn P.; Type Fixpoints: Iteration vs. Recursion, in: Proc. ACM SIGPLAN International Conference on Functional Programming, SIGPLAN Notices, 34(9), ACM Press, 1999, pp. 102–113.