Document Open Access Logo

A Curry-Howard Approach to Church's Synthesis

Authors Cécilia Pradic, Colin Riba

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2017.30.pdf
  • Filesize: 0.63 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • Intuitionistic Arithmetic
  • Realizability
  • Monadic Second-Order Logic on Infinite Words

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Cécilia 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

Author Details

Cécilia Pradic
Colin Riba

References

  1. 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. Google Scholar
  2. M. Bonsangue, J. Rutten, and A. Silva. Coalgebraic logic and synthesis of Mealy machines. In Proceedings of FOSSACS'08, pages 231-245. Springer, 2008. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. J.-Y. Girard. Interprétation Fonctionnelle et Élimination des Coupures de l'Arithmétique d'Ordre Supérieur. PhD thesis, Université Paris 7, 1972. Google Scholar
  7. 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. Google Scholar
  8. U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer, 2008. Google Scholar
  9. R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521-530, 1966. Google Scholar
  10. D. Perrin and J.-É. Pin. Infinite Words: Automata, Semigroups, Logic and Games. Pure and Applied Mathematics. Elsevier, 2004. Google Scholar
  11. M. O. Rabin. Automata on infinite objects and Church’s Problem. Amer. Math. Soc., 1972. Google Scholar
  12. 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. Google Scholar
  13. C. Riba. A Dialectica-Like Approach to Tree Automata. Available on HAL (hal-01261183), https://hal.archives-ouvertes.fr/hal-01261183, 2016.
  14. D. Siefkes. Decidable Theories I: Büchi’s Monadic Second Order Successor Arithmetic, volume 120 of LNM. Springer, 1970. Google Scholar
  15. The Coq Developement Team. The Coq Proof Assistant Reference Manual, 2016. URL: http://coq.inria.fr/.
  16. W. Thomas. Languages, Automata, and Logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume III, pages 389-455. Springer, 1997. Google Scholar
  17. W. Thomas. Solution of Church’s Problem: A tutorial. New Perspectives on Games and Interaction, 5:23, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact