Our goal in this paper is to analyze the interpretation of arbitrary unsolvable λ-terms in a given model of λ-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 β-reduces to a term admitting a decoration. The main result of this paper concerns the interconnection between those tow notions: given a graph model or stable model D, we show that any unsolvable term admitting a decoration and having a non-empty interpretation in D generates a critical sequence in the model. In the last section, we examine three classical graph models, namely the model B(ω) of Plotkin and Scott, Engeler's model D_A and Park's model D_p. We show that B(ω) and D_A do not contain critical sequences whereas D_p does.
展开▼
