Graph models of $\lambda$-calculus at work, and variations
| Autor: | Chantal Berline |
|---|---|
| Přispěvatelé: | Preuves, Programmes et Systèmes (PPS), Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7) |
| Rok vydání: | 2006 |
| Předmět: |
MSC 03B40
03C65 Scott's continuous semantics 0102 computer and information sciences Lambda 01 natural sciences Omega Combinatorics Mathematics (miscellaneous) untyped lambda-calculus 0101 mathematics Functional semantics Mathematics computer.programming_language Discrete mathematics lambda-theories graph semantics Graph models models of lambda-calculus 010102 general mathematics 16. Peace & justice Graph Computer Science Applications [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] 010201 computation theory & mathematics Lambda calculus computer |
| Zdroj: | Mathematical Structures in Computer Science Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2006, 16, pp.185-221. ⟨10.1017/S0960129506005123⟩ |
| ISSN: | 1469-8072 0960-1295 |
| DOI: | 10.1017/s0960129506005123 |
| Popis: | This paper surveys what we have learned during the last ten years about the lattice $\lambda \mathcal{T}$ of all $\lambda$-theories (= equational extensions of untyped $\lambda$-calculus), via the sets $\lambda \mathcal{C}$ consisting of the $\lambda$-theories that are representable in a uniform class $\mathcal{C}$ of $\lambda$-models. This includes positive answers to several questions raised in Berline (2000), as well as several independent results, the state of the art on the long-standing open questions concerning the representability of $\lambda _{\beta},\lambda _{\beta\eta}$, $H$ as theories of models, and 22 open problems.We will focus on the class $\mathcal{G}$ of graph models, since almost all the existing semantic proofs on $\lambda \mathcal{T}$ have been, or could be, more easily, obtained via graph models, or slight variations of them. But in this paper we will also give some evidence that, for all uniform classes $\mathcal{C},\mathcal{C}^{\prime}$ of proper $\lambda$-models living in functional semantics, $\lambda \mathcal{C}-\lambda \mathcal{C}^{\prime}$ should have cardinality $2^{\omega }$, provided $ \mathcal{C}$ is not included in $\mathcal{C}^{\prime}.$ |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|