A model for divergence insensitive properties of lambdaY-terms

Sylvain Salvati (1, 2) , Igor Walukiewicz (2)

1 PoSET - Models for a Structured Programming of Space and Time
2 LaBRI - Laboratoire Bordelais de Recherche en Informatique

A term of a simply typed λ-calculus with fixpoints can be considered as an abstraction of a higher-order functional program. The result of the computation of a term is its Böhm tree. Given a tree automaton describing a property of Böhm trees, we are interested in constructing a model recognizing the property, in a sense that the value of a term determines if its Böhm tree satisfies the property. We show how to construct models recognizing properties expressed by parity automata that cannot detect divergence. We call them Ω-blind parity automata, as the symbol Ω is used in Böhm trees to represent divergence; an automaton is Ω-blind when it has to accept Ω from every state. The models we construct resemble standard Scott models of latices of monotone functions, but application needs to be modified and the the fixpoint operator should be interpreted as a particular non-extremal fixpoint in a lattice.

Mots clés: lambda Y-calculus; MSOL properties of Bohm trees

Domaines: Logique en informatique [cs.LO]; Recherche d'information [cs.IR]

Sylvain Salvati, Igor Walukiewicz. A model for divergence insensitive properties of lambdaY-terms. 2015. ⟨hal-01169352⟩