DROPS

Document

Early Ideas

DOI: 10.4230/LIPIcs.CALCO.2021.21

Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas)

Authors: Koko Muroya, Takahiro Sanada, and Natsuki Urabe

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Abstract

We describe our ongoing work on generalizing some quantitatively constrained notions of weak simulation up-to that are recently introduced for deterministic systems modeling program execution. We present and discuss a new notion dubbed preorder-constrained simulation that allows comparison between words using a preorder, instead of equality.

Cite as

Koko Muroya, Takahiro Sanada, and Natsuki Urabe. Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 21:1-21:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{muroya_et_al:LIPIcs.CALCO.2021.21,
  author =	{Muroya, Koko and Sanada, Takahiro and Urabe, Natsuki},
  title =	{{Preorder-Constrained Simulation for Nondeterministic Automata}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{21:1--21:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.21},
  URN =		{urn:nbn:de:0030-drops-153762},
  doi =		{10.4230/LIPIcs.CALCO.2021.21},
  annote =	{Keywords: simulation, weak simulation, up-to technique, language inclusion, preorder}
}

Document

DOI: 10.4230/LIPIcs.CSL.2017.32

The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter

Authors: Koko Muroya and Dan R. Ghica

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract

Girard's Geometry of Interaction (GoI), a semantics designed for linear logic proofs, has been also successfully applied to programming languages. One way is to use abstract machines that pass a token in a fixed graph, along a path indicated by the GoI. These token-passing abstract machines are space efficient, because they handle duplicated computation by repeating the same moves of a token on the fixed graph. Although they can be adapted to obtain sound models with regard to the equational theories of various evaluation strategies for the lambda calculus, it can be at the expense of significant time costs. In this paper we show a token-passing abstract machine that can implement evaluation strategies for the lambda calculus, with certified time efficiency. Our abstract machine, called the Dynamic GoI Machine (DGoIM), rewrites the graph to avoid replicating computation, using the token to find the redexes. The flexibility of interleaving token transitions and graph rewriting allows the DGoIM to balance the trade-off of space and time costs. This paper shows that the DGoIM can implement call-by-need evaluation for the lambda calculus by using a strategy of interleaving token passing with as much graph rewriting as possible. Our quantitative analysis confirms that the DGoIM with this strategy of interleaving the two kinds of possible operations on graphs can be classified as “efficient” following Accattoli’s taxonomy of abstract machines.

Cite as

Koko Muroya and Dan R. Ghica. The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{muroya_et_al:LIPIcs.CSL.2017.32,
  author =	{Muroya, Koko and Ghica, Dan R.},
  title =	{{The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{32:1--32:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.32},
  URN =		{urn:nbn:de:0030-drops-76886},
  doi =		{10.4230/LIPIcs.CSL.2017.32},
  annote =	{Keywords: Geometry of Interaction, cost analysis, call-by-need reduction}
}

Search Results

Documents authored by Muroya, Koko

Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas)

Abstract

Cite as

The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter

Abstract

Cite as

Thanks for your feedback!

Could not send message