The Interpretation of Unsolvable $\lambda$-Terms in Models of Untyped $\lambda$-Calculus
Kerth, Rainer
J. Symbolic Logic, Tome 63 (1998) no. 1, p. 1529-1548 / Harvested from Project Euclid
Our goal in this paper is to analyze the interpretation of arbitrary unsolvable $\lambda$-terms in a given model of $\lambda$-calculus. We focus on graph models and (a special type of) stable models. We introduce the syntactical notion of a decoration and the semantical notion of a critical sequence. We conjecture that any unsolvable term $\beta$-reduces to a term admitting a decoration. The main result of this paper concerns the interconnection between those two notions: given a graph model or stable model $\mathfrak{D}$, we show that any unsolvable term admitting a decoration and having a non-empty interpretation in $\mathfrak{D}$ generates a critical sequence in the model. In the last section, we examine three classical graph models, namely the model $\mathfrak{B}(\omega)$ of Plotkin and Scott, Engeler's model $\mathfrak{D}_A$ and Park's model $\mathfrak{D}_P$. We show that $\mathfrak{B}(\omega)$ and $\mathfrak{D}_A$ do not contain critical sequences whereas $\mathfrak{D}_P$ does.
Publié le : 1998-12-14
Classification: 
@article{1183745646,
     author = {Kerth, Rainer},
     title = {The Interpretation of Unsolvable $\lambda$-Terms in Models of Untyped $\lambda$-Calculus},
     journal = {J. Symbolic Logic},
     volume = {63},
     number = {1},
     year = {1998},
     pages = { 1529-1548},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745646}
}
Kerth, Rainer. The Interpretation of Unsolvable $\lambda$-Terms in Models of Untyped $\lambda$-Calculus. J. Symbolic Logic, Tome 63 (1998) no. 1, pp.  1529-1548. http://gdmltest.u-ga.fr/item/1183745646/