We study iteration and recursion operators in the denotational semantics of typed λ-calculi derived from the multiset relational model of linear logic. Although these operators are defined as fixpoints of typed functionals, we prove them finitary in the sense of Ehrhard's finiteness spaces.
Mots-clés : higher order primitive recursion, denotational semantics
@article{ITA_2013__47_1_111_0, author = {Vaux, Lionel}, title = {A non-uniform finitary relational semantics of system $T$}, journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications}, pages = {111--132}, publisher = {EDP-Sciences}, volume = {47}, number = {1}, year = {2013}, doi = {10.1051/ita/2012031}, language = {en}, url = {http://archive.numdam.org/articles/10.1051/ita/2012031/} }
TY - JOUR AU - Vaux, Lionel TI - A non-uniform finitary relational semantics of system $T$ JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2013 SP - 111 EP - 132 VL - 47 IS - 1 PB - EDP-Sciences UR - http://archive.numdam.org/articles/10.1051/ita/2012031/ DO - 10.1051/ita/2012031 LA - en ID - ITA_2013__47_1_111_0 ER -
%0 Journal Article %A Vaux, Lionel %T A non-uniform finitary relational semantics of system $T$ %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2013 %P 111-132 %V 47 %N 1 %I EDP-Sciences %U http://archive.numdam.org/articles/10.1051/ita/2012031/ %R 10.1051/ita/2012031 %G en %F ITA_2013__47_1_111_0
Vaux, Lionel. A non-uniform finitary relational semantics of system $T$. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 47 (2013) no. 1, pp. 111-132. doi : 10.1051/ita/2012031. http://archive.numdam.org/articles/10.1051/ita/2012031/
[1] Linear-algebraic lambda-calculus : higher-order, encodings, and confluence, in Proc. 19th Int. Conf. on Rewriting Techniques and Applications, RTA 2008, Hagenberg, July 2008, edited by A. Voronkov. Springer. Lect. Notes Comput. Sci. 5117 (2008) 17-31. | MR | Zbl
and ,[2] Polynomial relators (extended abstract), in Proc. 2nd Int. Conf. on Algebraic Methodology and Software Technology, AMAST '91 (Iowa City, IO, May 1991), edited by M. Nivat, C. Rattray, T. Rus and G. Scollo. Springer. Workshops in Computing (1992) 303-326.
, , , , and ,[3] Generic properties of datatypes, in Generic Programming : Advanced Lectures, edited by R.C. Backhouse and J. Gibbons. Springer. Lect. Notes Comput. Sci. 2793 (2003) 97-132. | Zbl
and ,[4] Graph models of lambda-calculus at work, and variations. Math. Struct. Comput. Sci. 16 (2006) 185-221. | MR | Zbl
,[5] Stable models of typed lambda-calculi, in Proc. of 5th Int. Coll. on Automata, Languages and Programming, ICALP '78, Udine, July 1978, edited by G. Ausiello and C. Böhm. Springer. Lect. Notes Comput. Sci. 62 (1978) 72-89. | MR | Zbl
,[6] Not enough points is enough, in Proc. 21st Workshop on Computer Science Logic, CSL 2007, Lausanne, Sept. 2007, edited by J. Duparc, T. A. Henzinger. Springer. Lect. Notes Comput. Sci. 4646 (2007) 298-312. | MR | Zbl
, and ,[7] A relational model of a parallel and non-deterministic lambda-calculus, in Proc. Int. Symp. on Logical Foundations of Computer Science, LFCS 2009, Deerfield Beach, FL, Jan. 2009, edited by S.N. Artëmov and A. Nerode. Springer. Lect. Notes Comput. Sci. 5407 (2009) 107-121. | MR | Zbl
, and ,[8] On probabilistic coherence spaces, unpublished draft (2008). Available on http://hal.archives-ouvertes.fr/hal-00280462.
and ,[9] Sémantiques de la logique linéaire et temps de calcul, Ph.D. thesis, Université Aix-Marseille 2 (2007).
,[10] Execution time of lambda-terms via denotational semantics and intersection types. Technical report 6638. INRIA (2008).
,[11] Finiteness spaces. Math. Struct. Comput. Sci. 15 (2005) 615-646. | MR | Zbl
,[12] Interpreting a finitary pi-calculus in differential interaction nets. Inform. Comput. 208 (2010) 606-633. | MR | Zbl
and ,[13] The differential lambda-calculus. Theor. Comput. Sci. 309 (2003) 1-41. | MR | Zbl
and ,[14] Differential interaction nets. Electron. Notes Theoret. Comput. Sci. 123 (2005) 35-74. | MR | Zbl
and ,[15] Böhm trees, Krivine's machine and the Taylor expansion of λ-terms, in Proc. 2nd Conf. on Computability in Europe, CiE 2006, Swansea, June/July 2006, edited by A. Beckmann, U. Berger, B. Löwe and J.V. Tucker. Springer. Lect. Notes Comput. Sci. 3988 (2006) 186-197. | Zbl
and ,[16] The system F of variable types, fifteen years later. Theoret. Comput. Sci. 45 (1986) 159-192. | MR | Zbl
,[17] Linear logic. Theoret. Comput. Sci. 50 (1987) 1-102. | MR | Zbl
,[18] Normal functors, power series and lambda-calculus. Ann. Pure Appl. Log. 37 (1988) 129-177. | MR | Zbl
,[19] Proofs and Types, Cambridge University Press, Cambridge Tracts. Theoret. Comput. Sci. 7 (1989). | MR | Zbl
, and ,[20] Container types categorically. J. Funct. Program. 10 (2000) 191-225. | MR | Zbl
and ,[21] Glueing and orthogonality for models of linear logic. Theoret. Comput. Sci. 294 (2003) 183-231. | MR | Zbl
and ,[22] Introduction to Higher Order Categorical Logic, Cambridge University Press. Cambridge Stud. Adv. Math. 7 (1988). | MR | Zbl
and ,[23] Categorical semantics of linear logic. Société Mathématique de France. Interact. Models Comput. Program Behaviour Panor. 27 (2009) 1-196. | MR | Zbl
,[24] The inverse Taylor expansion problem in linear logic, in Proc. 24th Ann. IEEE Symp. on Logic in Computer Science, LICS '09, Los Angeles, CA, Aug. 2009. IEEE CS Press (2009) 222-231. | MR
and ,[25] On the representation of data in lambda-calculus, in Proc. of 3rd Workshop on Computer Science Logic, CSL '89, Kaiserslautern, Oct. 1989, edited by E. Börger, H. Kleine Büning and M.M. Richter. Springer. Lect. Notes Comput. Sci. 440 (1989) 309-321. | MR | Zbl
,[26] Data types as lattices. SIAM J. Comput. 5 (1976) 522-587. | MR | Zbl
,[27] Completeness, invariance and lambda-definability. J. Symb. Log. 47 (1982) 17-26. | MR | Zbl
,[28] Algebraic totality, towards completeness, in Proc. 9th Int. Conf. on Typed Lambda Calculi and Applications, TLCA 2009, Brasilia, July 2009, edited by P.-L. Curien. Springer. Lect. Notes Comput. Sci. 5608 (2009) 325-340. | MR | Zbl
,[29] Transport of finiteness structures and applications. Math. Struct. Comput. Sci. (to appear).
and ,[30] Pre-recursive categories. J. Pure Appl. Algebra 24 (1982) 79-93. | MR | Zbl
,[31] Intuitionistic differential nets and lambda-calculus. Theoret. Comput. Sci. 412 (2011) 1979-1997. | MR | Zbl
,[32] The algebraic lambda calculus. Math. Struct. Comput. Sci. 19 (2009) 1029-1059. | MR | Zbl
,[33] Differential linear logic and polarization, in Proc. 9th Int. Conf. on Typed Lambda Calculi and Applications, TLCA 2009. Brasilia, July 2009, edited by P.-L. Curien. Springer. Lect. Notes Comput. Sci. 5608 (2009) 371-385. | MR | Zbl
,Cité par Sources :