Parys, Pawel ;
Torunczyk, Szymon
Models of Lambda-Calculus and the Weak MSO Logic
Abstract
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.
BibTeX - Entry
@InProceedings{parys_et_al:LIPIcs:2016:6551,
author = {Pawel Parys and Szymon Torunczyk},
title = {{Models of Lambda-Calculus and the Weak MSO Logic}},
booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
pages = {11:1--11:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-022-4},
ISSN = {1868-8969},
year = {2016},
volume = {62},
editor = {Jean-Marc Talbot and Laurent Regnier},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6551},
URN = {urn:nbn:de:0030-drops-65511},
doi = {10.4230/LIPIcs.CSL.2016.11},
annote = {Keywords: typed lambda-calculus, models, weak MSO logic}
}
|
Keywords: |
|
typed lambda-calculus, models, weak MSO logic |
|
Seminar: |
|
25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
|
|
Issue date: |
|
2016 |
|
Date of publication: |
|
2016 |
2016
