摘要：We study the weak MSO logic in relationship to infinitary lambda-calculus. We show that for every formula phi of weak MSO there exists a finitary model of infinitary lambda-calculus recognizing the set of infinitary lambda-terms whose Böhm tree satisfies phi. The model is effective, in the sense that for every lambda-Y-term we can effectively compute its value in the model. In particular, given a finite lambda-Y-term, one can decide whether the resulting Böhm tree satisfies a given formula of weak MSO, which is a special case of the result of Ong, which concerns unrestricted MSO. The existence of effective models for weak MSO and MSO was proved earlier by Salvati and Walukiewicz but our proof uses a different method, as it does not involve automata, but works directly with logics.
