Recursive Domain Equations of Filter Models | SpringerLink
Skip to main content
Springer Nature Link
Log in

Recursive Domain Equations of Filter Models

  • Conference paper
SOFSEM 2008: Theory and Practice of Computer Science (SOFSEM 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4910))

Abstract

Filter models and (solutions of) recursive domain equations are two different ways of constructing lambda models. Many partial results have been shown about the equivalence between these two constructions (in some specific cases). This paper deepens the connection by showing that the equivalence can be shown in a general framework. We will introduce the class of disciplined intersection type theories and its four subclasses: natural split, lazy split, natural equated and lazy equated. We will prove that each class corresponds to a different recursive domain equation. For this result, we are extracting the essence of the specific proofs for the particular cases of intersection type theories and making one general construction that encompasses all of them. This general approach puts together all these results which may appear scattered and sometimes with incomplete proofs in the literature.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abramsky, S., Ong, L.C.: Full abstraction in the Lazy Lambda Calculus. Information and Computation 105, 159–267 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  2. Alessi, F.: Strutture di tipi, teoria dei domini, e modelli del λ-calcolo. PhD Thesis. University of Turin (1991)

    Google Scholar 

  3. Alessi, F., Dezani-Ciancaglini, M., Honsell, F.: Inverse Limit Models as Filter Models. In: Proceedings of HOR 2004, pp. 3–25 (2004)

    Google Scholar 

  4. Barendregt, H.P.: The Lambda Calculus: Its syntax and semantics. North-Holland Publishing co., Amsterdam (1984)

    MATH  Google Scholar 

  5. Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symbolic Logic 48(4), 931–940 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  6. Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Logic 21(4), 685–693 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  7. Coppo, M., Dezani-Ciancaglini, M., Longo, G.: Applicative information systems. In: Protasi, M., Ausiello, G. (eds.) CAAP 1983. LNCS, vol. 159, pp. 35–64. Springer, Heidelberg (1983)

    Google Scholar 

  8. Coppo, M., Dezani-Ciancaglini, M., Honsell, F., Longo, G.: Extended type structures and filter lambda models. In: Logic Colloquium 1982, pp. 241–262. North-Holland, Amsterdam (1984)

    Google Scholar 

  9. Coppo, M., Dezani-Ciancaglini, M., Zacchi, M.: Type theories, normal forms and D  ∞  lambda models. Information and Compuation 72(2), 85–116 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  10. Dezani-Ciancaglini, M., Ghilezan, S., Likavec, S.: Behavioural inverse limit models. Theoret. Comput. Sci. 316(1–3), 49–74 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  11. Dezani-Ciancaglini, M., Honsell, F., Alessi, F.: A complete characterization of complete intersection-type preorders. ACM TOCL 4(1), 120–146 (2003)

    Article  MathSciNet  Google Scholar 

  12. Dezani-Ciancaglini, M., Honsell, F., Motohama, Y.: Compositional characterization of λ-terms using intersection types. Theoret. Comput. Sci. 304(3), 459–495 (2005)

    Article  MathSciNet  Google Scholar 

  13. Gierz, G., Hofmann, K.H., Keimel, K., Lawson, D.J., Mislove, M.W., Scott, D.: Continuous lattices and domains. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  14. Hindley, R., Longo, G.: Lambda calculus models and extensionality. Z. Math Logik Grundlag. Math 26(4), 289–310 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  15. Honsell, F., Ronchi Della Rocca, S.: An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. J. Comput. System Sci. 45(1), 49–75 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  16. Park, D.: The Y-combinator in Scott’s λ-calculus models (revised version). Theory of Computation Report 13, Department of Computer Science, University of Warick (1976)

    Google Scholar 

  17. Plotikin, G.: Set-Theoretic and Other Elementary Models of the λ-Calculus. Theoretical Computer Science 121, 351–409 (1993)

    Article  MathSciNet  Google Scholar 

  18. Ronchi della Rocca, S., Paolini, L.: The Parametric Lambda Calculus. A Metamodel for Computation. In: Texts in Theoretical Computer Science. An EACTS Series, Springer, Heidelberg (2004)

    Google Scholar 

  19. Scott, D.S.: Domains for denotational semantics. In: Nielsen, M., Schmidt, E.M. (eds.) Automata, Languages, and Programming. LNCS, vol. 140, pp. 577–613. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  20. Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM Journal on Computing 11(4), 761–783 (1982)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Matematica ed Informatica, Università degli Studi di Udine, via delle Scienze 208, 33100, Udine, Italy

    Fabio Alessi & Paula Severi

Authors
  1. Fabio Alessi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paula Severi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Viliam Geffert Juhani Karhumäki Alberto Bertoni Bart Preneel Pavol Návrat Mária Bieliková

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alessi, F., Severi, P. (2008). Recursive Domain Equations of Filter Models . In: Geffert, V., Karhumäki, J., Bertoni, A., Preneel, B., Návrat, P., Bieliková, M. (eds) SOFSEM 2008: Theory and Practice of Computer Science. SOFSEM 2008. Lecture Notes in Computer Science, vol 4910. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77566-9_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-77566-9_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-77565-2

  • Online ISBN: 978-3-540-77566-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation