LIPIcs.FSCD.2017.30.pdf
- Filesize: 0.6 MB
- 16 pages
Document
A Curry-Howard Approach to Church's Synthesis
Authors
-
Part of:
Volume:
2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-08-30
Cite As Get BibTex
Pierre Pradic and Colin Riba. A Curry-Howard Approach to Church's Synthesis. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.FSCD.2017.30
Abstract
Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic over infinite words, Church's synthesis can theoretically be solved algorithmically using automata and games. We revisit Church's synthesis via the Curry-Howard correspondence by introducing SMSO, a non-classical subsystem of MSO, which is shown to be sound and complete w.r.t. synthesis thanks to an automata-based realizability model.
Subject Classification
Keywords
- Intuitionistic Arithmetic
- Realizability
- Monadic Second-Order Logic on Infinite Words
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive (1) designs. Journal of Computer and System Sciences, 78(3):911-938, 2012.
-
M. Bonsangue, J. Rutten, and A. Silva. Coalgebraic logic and synthesis of Mealy machines. In Proceedings of FOSSACS'08, pages 231-245. Springer, 2008.
-
J. R. Büchi. On a Decision Methond in Restricted Second-Order Arithmetic. In E. Nagel et al., editor, Logic, Methodology and Philosophy of Science (Proc. 1960 Intern. Congr.), pages 1-11. Stanford Univ. Press, 1962.
-
J. R. Büchi and L. H. Landweber. Solving Sequential Conditions by Finite-State Strategies. Transation of the American Mathematical Society, 138:367-378, 1969.
-
A. Church. Applications of recursive arithmetic to the problem of circuit synthesis. In Summaries of the SISL, volume 1, pages 3-50. Cornell Univ., 1957.
-
J.-Y. Girard. Interprétation Fonctionnelle et Élimination des Coupures de l'Arithmétique d'Ordre Supérieur. PhD thesis, Université Paris 7, 1972.
-
E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002.
-
U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer, 2008.
-
R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521-530, 1966.
-
D. Perrin and J.-É. Pin. Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics. Elsevier, 2004.
-
M. O. Rabin. Automata on infinite objects and Church’s Problem. Amer. Math. Soc., 1972.
-
C. Riba. A model theoretic proof of completeness of an axiomatization of monadic second-order logic on infinite words. In Proceedings of IFIP-TCS'12, 2012.
- C. Riba. A Dialectica-Like Approach to Tree Automata. Available on HAL (hal-01261183), https://hal.archives-ouvertes.fr/hal-01261183, 2016.
-
D. Siefkes. Decidable Theories I: Büchi’s Monadic Second Order Successor Arithmetic, volume 120 of LNM. Springer, 1970.
- The Coq Developement Team. The Coq Proof Assistant Reference Manual, 2016. URL: http://coq.inria.fr/.
-
W. Thomas. Languages, Automata, and Logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume III, pages 389-455. Springer, 1997.
-
W. Thomas. Solution of Church’s Problem: A tutorial. New Perspectives on Games and Interaction, 5:23, 2008.