Document Open Access Logo

Unsolvable Terms in Filter Models (Invited Talk)

Authors Mariangiola Dezani-Ciancaglini , Paola Giannini , Furio Honsell

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.3.pdf
  • Filesize: 0.89 MB
  • 24 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.3.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • λ-calculus
  • Intersection Types
  • Unsolvable Terms
  • Filter Models

Metrics

Abstract

Intersection type theories (itt’s) and filter models, i.e. λ-calculus models generated by itt’s, are reviewed in full generality. In this framework, which subsumes most λ-calculus models in the literature based on Scott-continuous functions, we discuss the interpretation of unsolvable terms. We give a necessary, but not sufficient, condition on an itt for the interpretation of some unsolvable term to be non-trivial in the filter model it generates. This result is obtained building on a type theoretic characterisation of the fine structure of unsolvables.

Cite As Get BibTex

Mariangiola Dezani-Ciancaglini, Paola Giannini, and Furio Honsell. Unsolvable Terms in Filter Models (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.3

Author Details

Mariangiola Dezani-Ciancaglini
  • Dipartimento di Informatica, Università di Torino, Italy
Paola Giannini
  • DiSSTE, Università del Piemonte Orientale, Vercelli, Italy
Furio Honsell
  • Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Università di Udine, Italy

Funding

  • Giannini, Paola: This original research has the financial support of the Università del Piemonte Orientale.

References

  1. Samson Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51(1-2):1-77, 1991. URL: https://doi.org/10.1016/0168-0072(91)90065-T.
  2. Samson Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105(2):159-267, 1993. URL: https://doi.org/10.1006/INCO.1993.1044.
  3. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds. PACMPL, 2(ICFP):94:1-94:30, 2018. URL: https://doi.org/10.1145/3236789.
  4. Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Tailoring filter models. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES, volume 3085 of LNCS, pages 17-33. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24849-1_2.
  5. Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Intersection types and lambda models. Theoretical Computer Science, 355(2):108-126, 2006. URL: https://doi.org/10.1016/j.tcs.2006.01.004.
  6. Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Furio Honsell. Filter models and easy terms. In Antonio Restivo, Simona Ronchi Della Rocca, and Luca Roversi, editors, ICTCS, volume 2202 of LNCS, pages 17-37. Springer, 2001. URL: https://doi.org/10.1007/3-540-45446-2_2.
  7. Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Stefania Lusin. Intersection types and domain operators. Theoretical Computer Science, 316(1):25-47, 2004. URL: https://doi.org/10.1016/J.TCS.2004.01.022.
  8. Fabio Alessi and Stefania Lusin. Simple easy terms. In Steffen van Bakel, editor, ITRS, volume 70 of ENTCS, pages 1-18. Elsevier, 2002. URL: https://doi.org/10.1016/S1571-0661(04)80487-0.
  9. Sandra Alves, Delia Kesner, and Miguel Ramos. Extending the quantitative pattern-matching paradigm. In Oleg Kiselyov, editor, APLAS, volume 15194 of LNCS, pages 84-105. Springer, 2024. URL: https://doi.org/10.1007/978-981-97-8943-6_5.
  10. Jos C. M. Baeten and Bas Boerboom. Omega can be anything it should not be. In Indagationes Mathematicae, volume 82(2), pages 111-120, 1979. URL: https://doi.org/10.1016/1385-7258(79)90016-7.
  11. Henk Barendregt. The Lambda Calculus - its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, Amsterdam, 1985. Google Scholar
  12. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931-940, 1983. URL: https://doi.org/10.2307/2273659.
  13. Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139032636.
  14. Erika De Benedetti and Simona Ronchi Della Rocca. Bounding normalization time through intersection types. In ITRS, volume 121 of EPTCS, pages 48-57. Open Publishing Association, 2012. URL: https://doi.org/10.4204/EPTCS.121.4.
  15. Alessandro Berarducci. Infinite λ-calculus and non-sensible models. In Aldo Ursini, editor, Logic and Algebra, pages 17:1-17:39. Routledge, 1996. URL: https://doi.org/10.1201/9780203748671-17.
  16. Alessandro Berarducci and Benedetto Intrigila. Church-Rosser lambda-theories, infinite lambda-terms and consistency problems. In Wilfrid Hodges, Martin Hyland, Charles Steinhorn, and John Truss, editors, Logic: from Foundations to Applications, chapter 2, pages 33-58. Clarendon Press, 1996. URL: https://arpi.unipi.it/handle/11568/46466.
  17. Alexis Bernadet and Stéphane Graham-Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4):1-46, 2013. URL: https://doi.org/10.2168/LMCS-9(4:3)2013.
  18. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25:433-464, 2017. URL: https://doi.org/10.1093/jigpal/jzx018.
  19. Mario Coppo, Mariangiola Dezani-Ciancaglini, Furio Honsell, and Giuseppe Longo. Extended type structures and filter lambda models. In G. Lolli, G. Longo, and A. Marcja, editors, Logic Colloquium '82, volume 112 of Studies in Logic and the Foundations of Mathematics, pages 241-262. Elsevier, 1984. URL: https://doi.org/10.1016/S0049-237X(08)71819-6.
  20. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Principal type schemes and lambda-calculus semantics. In Roger Hindley and Jonathan P. Seldin, editors, To H.B.Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, pages 535-560. Academic Press, 1980. URL: http://www.di.unito.it/~dezani/papers/CDV80.pdf.
  21. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Maddalena Zacchi. Type theories, normal forms and D_∞-lambda-models. Information and Computation, 72(2):85-116, 1987. URL: https://doi.org/10.1016/0890-5401(87)90042-3.
  22. Haskell B. Curry and Robert Feys. Combinatory Logic. North-Holland, Amsterdam, 1958. Google Scholar
  23. René David. Every unsolvable lambda term has a decoration. In Jean-Yves Girard, editor, TLCA, volume 1581 of LNCS, pages 98-113. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_9.
  24. Mariangiola Dezani-Ciancaglini, Besik Dundua, Paola Giannini, and Furio Honsell. Sensible intersection type theories. 2025. URL: https://people.unipmn.it/giannini/dgh25.pdf.
  25. Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, and Silvia Likavec. Behavioural inverse limit lambda-models. Theoretical Computer Science, 316(1):49-74, 2004. URL: https://doi.org/10.1016/J.TCS.2004.01.023.
  26. Mariangiola Dezani-Ciancaglini, Furio Honsell, and Yoko Motohama. Compositional characterisations of lambda-terms using intersection types. Theoretical Computer Science, 340(3):459-495, 2005. URL: https://doi.org/10.1016/J.TCS.2005.03.011.
  27. Mariangiola Dezani-Ciancaglini and Stefania Lusin. Intersection types and lambda theories. CoRR, cs.LO/0211011, 2002. URL: http://arxiv.org/abs/cs/0211011.
  28. Pietro Di Gianantonio, Furio Honsell, and Marina Lenisa. A type assignment system for game semantics. Theoretical Computer Science, 398(1):150-169, 2008. URL: https://doi.org/10.1016/j.tcs.2008.01.023.
  29. Erwin Engeler. Algebras and combinators. Algebra Universalis, 13:389-392, 1981. URL: https://doi.org/10.1007/BF02483849.
  30. Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, TACS, volume 789 of LNCS, pages 555-574. Springer, 1994. URL: https://doi.org/10.1007/3-540-57887-0_115.
  31. Pietro Di Gianantonio and Furio Honsell. An abstract notion of application. In Marc Bezem and Jan Friso Groote, editors, TLCA, volume 664 of LNCS, pages 124-138. Springer, 1993. URL: https://doi.org/10.1007/BFB0037102.
  32. Pietro Di Gianantonio and Marina Lenisa. Innocent game semantics via intersection type assignment systems. In Simona Ronchi Della Rocca, editor, CSL, volume 23 of LIPIcs, pages 231-247. Schloss Dagstuhl, 2013. URL: https://doi.org/10.4230/LIPICS.CSL.2013.231.
  33. Kurt Gödel, Solomon Feferman, John Dawson, Stephen Kleene, Gregory Moore, Robert Solovay, and Jean Heijenoort. Collected Works: Volume II Publications 1938-1974. Oxford University Press, June 2001. URL: https://doi.org/10.1093/oso/9780195147216.001.0001.
  34. Roger Hindley and Giuseppe Longo. Lambda calculus models and extensionality. Mathematical Logic Quarterly, 26(19-21):289-310, 1980. URL: https://doi.org/10.1002/malq.19800261902.
  35. Furio Honsell and Marina Lenisa. Semantical analysis of perpetual strategies in lambda-calculus. Theoretical Computer Science, 212(1-2):183-209, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00140-6.
  36. Furio Honsell and Marina Lenisa. "Wave-Style" geometry of interaction models in Rel are graph-like lambda-models. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, TYPES, volume 3085 of LNCS, pages 242-258. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24849-1_16.
  37. Furio Honsell and Gordon Plotkin. On the completeness of order-theoretic models of the λ-calculus. Information and Computation, 207, May 2009. URL: https://doi.org/10.1016/j.ic.2008.03.027.
  38. Furio Honsell and Simona Ronchi Della Rocca. Reasoning about interpretations in qualitative λ-models. In Manfred Broy and Cliff B. Jones, editors, Programming concepts and methods, pages 505-522. North-Holland, 1990. URL: https://people.uniud.it/sites/default/files/HR90.pdf.
  39. Furio Honsell and Simona Ronchi Della Rocca. An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences, 45(1):49-75, 1992. URL: https://doi.org/10.1016/0022-0000(92)90040-P.
  40. Giuseppe Jacopini. A condition for identifying two elements of whatever model of combinatory logic. In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, volume 37 of LNCS, pages 213-219. Springer, 1975. URL: https://doi.org/10.1007/BFB0029527.
  41. Rainer Kerth. The interpretation of unsolvable λ-terms in models of untyped λ-calculus. Journal of Symbolic Logic, 63(4):1529-1548, 1998. URL: https://doi.org/10.2307/2586665.
  42. Assaf J. Kfoury. A linearization of the lambda-calculus and consequences. Journal of Logic and Computation, 10(3):411-436, 2000. URL: https://doi.org/10.1093/LOGCOM/10.3.411.
  43. Jean-Jacques Lévy. An algebraic interpretation of the lambda beta-calculus and a labeled lambda-calculus. In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, volume 37 of LNCS, pages 147-165. Springer, 1975. URL: https://doi.org/10.1007/BFB0029523.
  44. Giuseppe Longo. Set-theoretical models of λ-calculus: theories, expansions, isomorphisms. Annals of Pure and Applied Logic, 24(2):153-188, 1983. URL: https://doi.org/10.1016/0168-0072(83)90030-1.
  45. Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Logical semantics for stability. In Samson Abramsky, Michael W. Mislove, and Catuscia Palamidessi, editors, MFPS, volume 249 of ENTCS, pages 429-449. Elsevier, 2009. URL: https://doi.org/10.1016/J.ENTCS.2009.07.101.
  46. David Park. The Y-combinator in Scott’s lambda-calculus models. Theory of Computation Report, University of Warwick. Department of Computer Science, 1976. URL: http://wrap.warwick.ac.uk/46310/.
  47. Gordon D. Plotkin. Set-theoretical and other elementary models of the lambda-calculus. Theoretical Computer Science, 121(1&2):351-409, 1993. URL: https://doi.org/10.1016/0304-3975(93)90094-A.
  48. Simona Ronchi Della Rocca and Luca Paolini. The Parametric Lambda Calculus - A Metamodel for Computation. EATCS. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-10394-4.
  49. Dana Scott. Continuous lattices. In Francis William Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of LNM, pages 97-136. Springer, 1972. URL: https://doi.org/10.1007/BFb0073967.
  50. Dana S. Scott. Open problem n. II 4. In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, volume 37 of LNCS, page 369. Springer, 1975. URL: https://doi.org/10.1007/BFb0029538.
  51. Dana S. Scott. Data types as lattices. SIAM Journal on Computing, 5(3):522-587, 1976. URL: https://doi.org/10.1137/0205037.
  52. Jeremy G. Siek. Revisiting elementary denotational semantics. CoRR, abs/2312.02359, 2017. URL: https://doi.org/10.48550/arXiv.1707.03762.
  53. Makoto Tatsuta and Mariangiola Dezani-Ciancaglini. Normalisation is insensible to lambda-term identity or difference. In LICS, pages 327-338. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.36.
  54. Cécile Zylberajch. Syntaxe et semantique de la facilité en lambda calcul. PhD thesis, Université de Paris VII, 1991. URL: https://theses.fr/1991PA077272.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact