Two extensions of system F with (co)iteration and primitive (co)recursion principles

Favio Ezequiel Miranda-Perea

RAIRO - Theoretical Informatics and Applications (2009)

  • Volume: 43, Issue: 4, page 703-766
  • ISSN: 0988-3754

Abstract

top
This paper presents two extensions of the second order polymorphic lambda calculus, system F, with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism. The systems are presented in Curry-style, and are proven to be terminating and type-preserving. Moreover their expressiveness is shown by means of several programming examples, going from usual data types to lazy codata types such as streams or infinite trees.

How to cite

top

Miranda-Perea, Favio Ezequiel. "Two extensions of system F with (co)iteration and primitive (co)recursion principles." RAIRO - Theoretical Informatics and Applications 43.4 (2009): 703-766. <http://eudml.org/doc/250595>.

@article{Miranda2009,
abstract = { This paper presents two extensions of the second order polymorphic lambda calculus, system F, with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism. The systems are presented in Curry-style, and are proven to be terminating and type-preserving. Moreover their expressiveness is shown by means of several programming examples, going from usual data types to lazy codata types such as streams or infinite trees. },
author = {Miranda-Perea, Favio Ezequiel},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Coiteration; corecursion; iteration; primitive recursion; system F; monotone inductive type; monotone coinductive type; monotonicity witness; saturated sets; algebras; coalgebras; dialgebras.; coiteration; System F; monotonicity witness; dialgebras},
language = {eng},
month = {9},
number = {4},
pages = {703-766},
publisher = {EDP Sciences},
title = {Two extensions of system F with (co)iteration and primitive (co)recursion principles},
url = {http://eudml.org/doc/250595},
volume = {43},
year = {2009},
}

TY - JOUR
AU - Miranda-Perea, Favio Ezequiel
TI - Two extensions of system F with (co)iteration and primitive (co)recursion principles
JO - RAIRO - Theoretical Informatics and Applications
DA - 2009/9//
PB - EDP Sciences
VL - 43
IS - 4
SP - 703
EP - 766
AB - This paper presents two extensions of the second order polymorphic lambda calculus, system F, with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism. The systems are presented in Curry-style, and are proven to be terminating and type-preserving. Moreover their expressiveness is shown by means of several programming examples, going from usual data types to lazy codata types such as streams or infinite trees.
LA - eng
KW - Coiteration; corecursion; iteration; primitive recursion; system F; monotone inductive type; monotone coinductive type; monotonicity witness; saturated sets; algebras; coalgebras; dialgebras.; coiteration; System F; monotonicity witness; dialgebras
UR - http://eudml.org/doc/250595
ER -

References

top
  1. A. Abel, R. Matthes and T. Uustalu, Iteration and coiteration schemes for higher-order and nested datatypes. Theoret. Comput. Sci.333 (2005) 3–66.  
  2. C. Böhm and A Berarducci, Automatic synthesis of typed Λ-programs on term algebras. Theoret. Comput. Sci.39 (1985) 135–154.  
  3. R.L. Crole, Categories for Types. Cambridge Mathematical Textbooks. Cambridge University Press (1993).  
  4. M.A. Cunha, Recursion patterns as hylomorphisms. Technical Report DI-PURe-03.11.01, Department of Informatics, University of Minho (2003).  
  5. B.A. Davey and H.A. Priestley, Introduction to Lattices and Order, 2nd edn. Cambridge University Press (2002).  
  6. H. Dybkjær and A. Melton, Comparing Hagino's categorical programming language and typed lambda-calculi. Theoret. Comput. Sci.111 (1991) 145–189.  
  7. H. Geuvers, Inductive and coinductive types with iteration and recursion. In Proceedings of the 1992 workshop on types for proofs and programs, Båstad, Sweden. Edited by B. Nordström, K. Petterson, G. Plotkin (1992) 183–207. Available via herman/BRABasInf_RecTyp.ps.gz.  URIhttp://www.cs.kun.nl/
  8. J. Gibbons and G. Jones, The under-appreciated unfold. In Proceedings 3rd ACM SIGPLAN international conference on functional programming, Baltimore, Maryland (1998) 273–279.  
  9. J.Y. Girard, Une extension de l'interpretation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types. Second Scandinavian Logic Symposium. Edited by J.E. Fenstad. North-Holland (1971) 63–92.  
  10. J.Y. Girard, Interprétation fonctionnelle et élimination des coupures dans l'arithmetique d'ordre supérieur. Thèse de Doctorat d'État, Université de Paris VII (1972).  
  11. J.Y. Girard, Y. Lafont and P. Taylor, Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1989).  
  12. J. Greiner, Programming with inductive and co-inductive types. Technical Report CMU-CS-92-109, Carnegie-Mellon University (1992)  
  13. T. Hagino, A typed lambda calculus with categorical type constructors. In Category Theory and Computer Science. Edited by D.H. Pitt, A. Poigné and D.E. Rydeheard. Lect. Notes Comput. Sci.283 (1987).  
  14. T. Hagino, A Categorical programming language. Ph.D. Thesis CST-47-87 (also published as ECS-LFCS-87-38). Department of Computer Science, University of Edinburgh (1987).  
  15. B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. EATCS Bull.62 (1997) 222–259.  
  16. J. Kabanov and V. Vene, Recursion schemes for dynamic programming. In Proc. 8th Int. Conf. on Mathematics of Program Construction, MPC 06. Edited by T. Uustalu. Lect. Notes Comput. Sci.4014 (2006) 235–252.  
  17. J.L. Krivine, Lambda-calculus, types and models. Ellis Horwood Series in Computers and their Applications. Ellis Horwood, Masson (1993).  
  18. S. Mac Lane, Categories for the Working Mathematician, 2nd. edn., Vol. 5. Graduate Texts in Mathematics. Springer Verlag (1998).  
  19. R. Matthes, Extensions of system F by iteration and primitive recursion on monotone inductive types. Dissertation Universität München (1999). Available via matthes/dissertation/ matthesdiss.ps.gz  URIhttp://www.tcs.informatik.uni-muenchen.de/
  20. R. Matthes, Monotone (co)inductive types and positive fixed-point types. RAIRO-Theor. Inf. Appl.33 (1999) 309–328.  
  21. R. Matthes, Monotone fixed-point types and strong normalization. In Computer Science Logic. Edited by G. Gottlob, E. Grandjean, K. Seyr. 12th International Workshop, Brno, Czech Republic, August 24–28, 1998. Lect. Notes Comput. Sci.1584 (1999) 298–312.  
  22. R. Matthes, Monotone inductive and coinductive constructors of rank 2. In Computer Science Logic 2001. Lect. Notes Comput. Sci.2142 (2001) 600–614.  
  23. R. Matthes, Non-strictly positive fixed-points for classical natural deduction. Ann. Pure Appl. Logic133 (2005) 205–230.  
  24. E. Meijer, M. Fokkinga and R. Paterson, Functional programming with bananas, lenses, envelopes and barbed wire. In FPCA 91. Edited by J. Hughes. Lect. Notes Comput. Sci.523 (1991) 124–144.  
  25. N.P. Mendler, Recursive types and type constraints in second-order lambda calculus. In Proceedings of the 2nd Annual Symposium on Logic in Computer Science, Ithaca, N.Y. IEEE Computer Society Press, Washington D.C. (1987) 30–36.  
  26. N.P. Mendler, Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Logic51 (1991) 159–172.  
  27. F.E. Miranda-Perea, On extensions of AF2 with monotone and clausular (co)inductive definitions. Ph.D. Thesis, Ludwig-Maximilians-Universität München, Germany (2004).  
  28. F.E. Miranda-Perea, Some remarks on type systems for course-of-value recursion. In Proceedings of the third workshop on Logical and Semantic Frameworks with Applications (LSFA 2008). Electronic Notes in Theoretical Computer Science 247 (2009).  
  29. M. Parigot, Recursive programming with proofs. Theoret. Comput. Sci.94 (1992) 335–356.  
  30. E. Poll and J. Zwanenburg, From algebras and coalgebras to dialgebras. In Coalgebraic Methods in Computer Science (CMCS'2001). Electronic Notes in Theoretical Computer Science44 (2001).  
  31. J. Reynolds, Towards a theory of type structure. In Proc. Colloque sur la Programmation. Edited by B. Robinet. Lect. Notes Comput. Sci.19 (1974).  
  32. J.J.M.M. Rutten, Automata and coinduction (an exercise in coalgebra). In Proceedings of CONCUR '98. Edited by D. Sangiorgi and R. de Simone. Lect. Notes Comput. Sci.1466 (1998) 194–218.  
  33. Z. Spławski and P. Urzyczyn, Type fixpoints: iteration vs. recursion. In Proc. International Conference on Functional Programming. ACM Press (1999), pp 102–113.  
  34. W.W. Tait, A realizability interpretation of the theory of species. In Logic Colloquium Boston 1971/72. Edited by R. Parikh. Lect. Notes Math.453 (1975) 240–251.  
  35. D. Turner, Total functional programming. J. Universal Comput. Sci.10 (2004) 751–768.  
  36. T. Uustalu and V. Vene, Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica10 (1999) 5–26.  
  37. T. Uustalu and V. Vene, Least and greatest fixed-points in intuitionistic natural deduction. Theoret. Comput. Sci.272 (2002) 315–339.  
  38. V. Vene, Categorical programming with inductive and coinductive types. Diss. Math. Univ. Tartuensis23, Univ. Tartu (2000).  
  39. P. Wadler, Theorems for free. In Proc. 4th international conference on functional programming languages and computer architecture. Imperial College, London (1989), pp 347–359.  
  40. G.C. Wraith, A note on categorical datatypes. In Category Theory and Computer Science. Edited by D. Pitts et al.Lect. Notes Comput. Sci.389 (1989).  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.