When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2016.11
URN: urn:nbn:de:0030-drops-65511
Go to the corresponding LIPIcs Volume Portal

Parys, Pawel ; Torunczyk, Szymon

Models of Lambda-Calculus and the Weak MSO Logic

LIPIcs-CSL-2016-11.pdf (1 MB)


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

  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 =		{},
  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: 25.08.2016

DROPS-Home | Fulltext Search | Imprint Published by LZI