eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2016-08-29
11:1
11:12
10.4230/LIPIcs.CSL.2016.11
article
Models of Lambda-Calculus and the Weak MSO Logic
Parys, Pawel
Torunczyk, Szymon
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol062-csl2016/LIPIcs.CSL.2016.11/LIPIcs.CSL.2016.11.pdf
typed lambda-calculus
models
weak MSO logic