A non-uniform finitary relational semantics of system T

Lionel Vaux

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2013)

  • Volume: 47, Issue: 1, page 111-132
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

Vaux, Lionel. "A non-uniform finitary relational semantics of system T." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 47.1 (2013): 111-132. <http://eudml.org/doc/273067>.

@article{Vaux2013,
abstract = {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.},
author = {Vaux, Lionel},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {higher order primitive recursion; denotational semantics; Gödel System T; lazy semantics; relational semantics; finiteness space},
language = {eng},
number = {1},
pages = {111-132},
publisher = {EDP-Sciences},
title = {A non-uniform finitary relational semantics of system T},
url = {http://eudml.org/doc/273067},
volume = {47},
year = {2013},
}

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
PB - EDP-Sciences
VL - 47
IS - 1
SP - 111
EP - 132
AB - 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.
LA - eng
KW - higher order primitive recursion; denotational semantics; Gödel System T; lazy semantics; relational semantics; finiteness space
UR - http://eudml.org/doc/273067
ER -

References

top
  1. [1] P. Arrighi and G. Dowek, 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. Zbl1146.68027MR2503407
  2. [2] R.C. Backhouse, P.J. de Bruin, P.F. Hoogendijk, G. Malcolm, E. Voermans and J. van der Woude, 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. 
  3. [3] R.C. Backhouse and P.F. Hoogendijk, 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. Zbl1274.68210
  4. [4] C. Berline, Graph models of lambda-calculus at work, and variations. Math. Struct. Comput. Sci.16 (2006) 185–221. Zbl1097.03011MR2228853
  5. [5] G. Berry, 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. Zbl0382.68041MR520840
  6. [6] A. Bucciarelli, T. Ehrhard and G. Manzonetto, 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. Zbl1179.03021MR2540209
  7. [7] A. Bucciarelli, T. Ehrhard and G. Manzonetto, 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. Zbl1211.03026MR2544240
  8. [8] V. Danos and T. Ehrhard, On probabilistic coherence spaces, unpublished draft (2008). Available on http://hal.archives-ouvertes.fr/hal-00280462. Zbl1267.68085
  9. [9] D. de Carvalho, Sémantiques de la logique linéaire et temps de calcul, Ph.D. thesis, Université Aix-Marseille 2 (2007). 
  10. [10] D. de Carvalho, Execution time of lambda-terms via denotational semantics and intersection types. Technical report 6638. INRIA (2008). 
  11. [11] T. Ehrhard, Finiteness spaces. Math. Struct. Comput. Sci.15 (2005) 615–646. Zbl1084.03048MR2158033
  12. [12] T. Ehrhard and O. Laurent, Interpreting a finitary pi-calculus in differential interaction nets. Inform. Comput.208 (2010) 606–633. Zbl1205.68242MR2663520
  13. [13] T. Ehrhard and L. Regnier, The differential lambda-calculus. Theor. Comput. Sci.309 (2003) 1–41. Zbl1070.68020MR2016523
  14. [14] T. Ehrhard and L. Regnier, Differential interaction nets. Electron. Notes Theoret. Comput. Sci.123 (2005) 35–74. Zbl1113.03054MR2207408
  15. [15] T. Ehrhard and L. Regnier, 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. Zbl1130.68054
  16. [16] J.-Y. Girard, The system F of variable types, fifteen years later. Theoret. Comput. Sci.45 (1986) 159–192. Zbl0623.03013MR867281
  17. [17] J.-Y. Girard, Linear logic. Theoret. Comput. Sci.50 (1987) 1–102. Zbl0625.03037MR899269
  18. [18] J.-Y. Girard, Normal functors, power series and lambda-calculus. Ann. Pure Appl. Log.37 (1988) 129–177. Zbl0646.03056MR926748
  19. [19] J.-Y. Girard, P. Taylor and Y. Lafont, Proofs and Types, Cambridge University Press, Cambridge Tracts. Theoret. Comput. Sci. 7 (1989). Zbl0671.68002MR1003608
  20. [20] P. Hoogendijk and O. De Moor, Container types categorically. J. Funct. Program.10 (2000) 191–225. Zbl0959.68023MR1767938
  21. [21] M. Hyland and A. Schalk, Glueing and orthogonality for models of linear logic. Theoret. Comput. Sci.294 (2003) 183–231. Zbl1029.03051MR1964781
  22. [22] J. Lambek and P.J. Scott, Introduction to Higher Order Categorical Logic, Cambridge University Press. Cambridge Stud. Adv. Math. 7 (1988). Zbl0642.03002MR939612
  23. [23] P.-A. Melliès, Categorical semantics of linear logic. Société Mathématique de France. Interact. Models Comput. Program Behaviour Panor.27 (2009) 1–196. Zbl1206.03052MR2675257
  24. [24] M. Pagani and C. Tasson, 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. MR2932387
  25. [25] M. Parigot, 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. Zbl0925.03149MR1079086
  26. [26] D.S. Scott, Data types as lattices. SIAM J. Comput.5 (1976) 522–587. Zbl0337.02018MR437330
  27. [27] R. Statman, Completeness, invariance and lambda-definability. J. Symb. Log.47 (1982) 17–26. Zbl0487.03006MR644749
  28. [28] C. Tasson, 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. Zbl1246.03081MR2550057
  29. [29] C. Tasson and L. Vaux, Transport of finiteness structures and applications. Math. Struct. Comput. Sci. (to appear). 
  30. [30] M.-F. Thibault, Pre-recursive categories. J. Pure Appl. Algebra24 (1982) 79–93. Zbl0485.18005MR647582
  31. [31] P. Tranquilli, Intuitionistic differential nets and lambda-calculus. Theoret. Comput. Sci.412 (2011) 1979–1997. Zbl1223.03049MR2814770
  32. [32] L. Vaux, The algebraic lambda calculus. Math. Struct. Comput. Sci.19 (2009) 1029–1059. Zbl1186.03025MR2545510
  33. [33] L. Vaux, 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. Zbl1246.03082MR2550060

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.