Document Open Access Logo

Towards Constructive Hybrid Semantics

Authors Tim Lukas Diezel, Sergey Goncharov

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.24.pdf
  • Filesize: 0.61 MB
  • 19 pages

Document Identifiers

Author Details

Tim Lukas Diezel
  • FAU Erlangen-Nürnberg, Germany
Sergey Goncharov
  • FAU Erlangen-Nürnberg, Germany

Funding

  • Goncharov, Sergey: Support by Deutsche Forschungsgemeinschaft (DFG) under project GO 2161/1-2 is gratefully acknowledged.

Acknowledgements

We would like to thank anonymous referees for carefully reading the text and making various points which contributed to improving presentation, and also to Stefan Milius for references on conservative completion.

Cite AsGet BibTex

Tim Lukas Diezel and Sergey Goncharov. Towards Constructive Hybrid Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.24

Abstract

With hybrid systems becoming ever more pervasive, the underlying semantic challenges emerge in their entirety. The need for principled semantic foundations has been recognized previously in the case of discrete computation and discrete data, with subsequent implementations in programming languages and proof assistants. Hybrid systems, contrastingly, do not directly fit into the classical semantic paradigms due to the presence of quite specific "non-programmable" features, such as Zeno behaviour and the inherent indispensable reliance on a notion of continuous time. Here, we analyze the phenomenon of hybrid semantics from a constructive viewpoint. In doing so, we propose a monad-based semantics, generic over a given ordered monoid representing the time domain, hence abstracting from the monoid of constructive reals. We implement our construction as a higher inductive-inductive type in the recent cubical extension of the Agda proof assistant, significantly using state-of-the-art advances of homotopy type theory. We show that classically, i.e. under the axiom of choice, our construction admits a charaterization in terms of directed sequence completion.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Axiomatic semantics
Keywords
  • Hybrid semantics
  • Elgot iteration
  • Homotopy type theory
  • Agda

Metrics

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

Supplementary Materials

References

  1. Samson Abramsky and Achim Jung. Domain theory. In Handbook of Logic in Computer Science, volume 3, pages 1-168. Oxford University Press, 1994. Google Scholar
  2. Jiří Adámek, Horst Herrlich, and George Strecker. Abstract and concrete categories. John Wiley & Sons Inc., New York, 1990. Google Scholar
  3. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. Quotient inductive-inductive types. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures, pages 293-310, Cham, 2018. Springer International Publishing. Google Scholar
  4. Thorsten Altenkirch, Nils Danielsson, and Nicolai Kraus. Partiality, revisited - the partiality monad as a quotient inductive-inductive type. In Javier Esparza and Andrzej Murawski, editors, Foundations of Software Science and Computation Structures, FOSSACS 2017, volume 10203 of LNCS, pages 534-549, 2017. Google Scholar
  5. Abhishek Anand and Ross Knepper. ROSCoq: Robots powered by constructive reals. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving, pages 34-50, Cham, 2015. Springer International Publishing. Google Scholar
  6. James Chapman, Tarmo Uustalu, and Niccolò Veltri. Quotienting the delay monad by weak bisimilarity. In Theoretical Aspects of Computing, ICTAC 2015, volume 9399 of LNCS, pages 110-125. Springer, 2015. Google Scholar
  7. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  8. Nils Anders Danielsson. Code related to the paper "Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type". http://www.cse.chalmers.se/~nad/listings/partiality-monad/. Accessed: 2020-02-12. URL: http://www.cse.chalmers.se/~nad/listings/partiality-monad/.
  9. Sergey Goncharov, Julian Jakob, and Renato Neves. A semantics for hybrid iteration. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory (CONCUR 2018), LNCS. Springer, 2018. Google Scholar
  10. Sergey Goncharov and Renato Neves. An adequate while-language for hybrid computation. In Ekaterina Komendantskaya, editor, Proceedings of the 21th International Symposium on Principles and Practice of Declarative Programming, (PPDP 2019). ACM, 2019. Google Scholar
  11. Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Julian Jakob. Unguarded recursion on coinductive resumptions. Logical Methods in Computer Science, 14(3), 2018. Google Scholar
  12. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Inf. & Comp, 185:2003, 2002. Google Scholar
  13. Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971. Google Scholar
  14. Georg Markowsky. Chain-complete posets and directed sets with applications. Algebra universalis, 6:53-68, 1976. Google Scholar
  15. John C. Mitchell. Foundations of Programming Languages. MIT Press, Cambridge, MA, USA, 1996. Google Scholar
  16. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93:55-92, 1991. Google Scholar
  17. G. Plotkin. Post graduate lecture notes on advanced domain theory (incorporating the "Pisa notes"). Dept. of Computer Science, Univ. Edinburgh, 1981. Google Scholar
  18. J. Reynolds. Theories of Programming Languages. Cambridge University Press, 1998. Google Scholar
  19. Benjamin Sherman, Luke Sciarappa, Adam Chlipala, and Michael Carbin. Computable decision making on the reals and other spaces: Via partiality and nondeterminism. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 859-868, New York, NY, USA, 2018. ACM. Google Scholar
  20. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book.
  21. Niccoló Veltri. A Type-Theoretical Study of Nontermination. PhD thesis, Tallinn University of Technology, 2017. Google Scholar
  22. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Proceedings of the ACM on Programming Languages, 3(ICFP):87, 2019. Google Scholar
  23. Wolfgang Wechler. Universal Algebra for Computer Scientists, volume 25 of EATCS Monographs on Theoretical Computer Science. Springer, 1992. Google Scholar
  24. G. Winskel. The Formal Semantics of Programming Languages. MIT Press, Cambridge, Massachusetts, 1993. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact