2024

Correspondence Between Composite Theories and Distributive Laws

RossetAloı̈s, Maaike Zwart, Helle Hvid Hansen, and Jörg Endrullis

In: Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Luxembourg City, Luxembourg, April 6-7, 2024, Proceedings König, Barbara and Urbat, Henning (eds.) , pp. 194–215 , Springer (2024)

summary paper bib doi

Summary

Composite theories are the algebraic equivalent of distributive laws. In this paper, we delve into the details of this correspondence and concretely show how to construct a composite theory from a distributive law and vice versa. Using term rewriting methods, we also describe when a minimal set of equations axiomatises the composite theory.

Bibtex

@inproceedings{monads:composite:theories:2024,
  author = {Rosset, Alo{\"{\i}}s and Zwart, Maaike and Hansen, Helle Hvid and Endrullis, J{\"{o}}rg},
  editor = {K{\"{o}}nig, Barbara and Urbat, Henning},
  title = {Correspondence Between Composite Theories and Distributive Laws},
  booktitle = {Coalgebraic Methods in Computer Science - 17th {IFIP} {WG} 1.3 International
                    Workshop, {CMCS} 2024, Colocated with {ETAPS} 2024, Luxembourg City,
                    Luxembourg, April 6-7, 2024, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {14617},
  pages = {194--215},
  publisher = {Springer},
  year = {2024},
  url = {https://doi.org/10.1007/978-3-031-66438-0\_10},
  doi = {10.1007/978-3-031-66438-0\_10},
  biburl = {https://dblp.org/rec/conf/cmcs/RossetZHE24.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {coalgebra, rewriting},
  type = {workshop}
}

Digital Object Identifier

10.1007/978-3-031-66438-0_10

2022

Algebraic Presentation of Semifree Monads
RossetAloı̈s, Helle Hvid Hansen, and Jörg Endrullis
In: Coalgebraic Methods in Computer Science - 16th IFIP WG 1.3 International Workshop, CMCS 2022, Colocated with ETAPS 2022, Munich, Germany, April 2-3, 2022, Proceedings Hansen, Helle Hvid and Zanasi, Fabio (eds.) , pp. 110–132 , Springer (2022)
summary paper bib doi

Summary

Monads and their composition via distributive laws have many applications in program semantics and functional programming. For many interesting monads, distributive laws fail to exist, and this has motivated investigations into weaker notions. In this line of research, Petrişan and Sarkis recently introduced a construction called the semifree monad in order to study semialgebras for a monad and weak distributive laws. In this paper, we prove that an algebraic presentation of the semifree monad M^s on a monad M can be obtained uniformly from an algebraic presentation of M. This result was conjectured by Petrişan and Sarkis. We also show that semifree monads are ideal monads, that the semifree construction is not a monad transformer, and that the semifree construction is a comonad on the category of monads.
Bibtex
```
@inproceedings{monads:semifree:2022,
  author = {Rosset, Alo{\"{\i}}s and Hansen, Helle Hvid and Endrullis, J{\"{o}}rg},
  editor = {Hansen, Helle Hvid and Zanasi, Fabio},
  title = {Algebraic Presentation of Semifree Monads},
  booktitle = {Coalgebraic Methods in Computer Science - 16th {IFIP} {WG} 1.3 International
                    Workshop, {CMCS} 2022, Colocated with {ETAPS} 2022, Munich, Germany,
                    April 2-3, 2022, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {13225},
  pages = {110--132},
  publisher = {Springer},
  year = {2022},
  url = {https://doi.org/10.1007/978-3-031-10736-8\_6},
  doi = {10.1007/978-3-031-10736-8\_6},
  biburl = {https://dblp.org/rec/conf/cmcs/RossetHE22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {coalgebra},
  type = {workshop}
}
```
Digital Object Identifier
```
10.1007/978-3-031-10736-8_6
```
A PBPO+ Graph Rewriting Tutorial
Roy Overbeek, and Jörg Endrullis
In: Proceedings Twelfth International Workshop on Computing with Terms and Graphs, TERMGRAPH@FSCD 2022, Technion, Haifa, Israel, 1st August 2022 Grabmayer, Clemens (ed.) , pp. 45–63 (2022)
summary paper bib doi

Summary

We provide a tutorial introduction to the algebraic graph rewriting formalism PBPO+. We show how PBPO+ can be obtained by composing a few simple building blocks, and model the reduction rules for binary decision diagrams as an example. Along the way, we comment on how alternative design decisions lead to related formalisms in the literature, such as DPO. We close with a detailed comparison with Bauderon's double pullback approach.
Bibtex
```
@inproceedings{graph:rewriting:pbpo:tutorial:2022,
  author = {Overbeek, Roy and Endrullis, J{\"{o}}rg},
  editor = {Grabmayer, Clemens},
  title = {A {PBPO+} Graph Rewriting Tutorial},
  booktitle = {Proceedings Twelfth International Workshop on Computing with Terms
                    and Graphs, TERMGRAPH@FSCD 2022, Technion, Haifa, Israel, 1st August
                    2022},
  series = {{EPTCS}},
  volume = {377},
  pages = {45--63},
  year = {2022},
  url = {https://doi.org/10.4204/EPTCS.377.3},
  doi = {10.4204/EPTCS.377.3},
  biburl = {https://dblp.org/rec/journals/corr/abs-2301-12912.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting},
  type = {workshop}
}
```
Digital Object Identifier
```
10.4204/EPTCS.377.3
```

2021

From Linear Term Rewriting to Graph Rewriting with Preservation Of Termination
Roy Overbeek, and Jörg Endrullis
In: Proceedings Twelfth International Workshop on Graph Computational Models, GCM@STAF 2021, Online, 22nd June 2021 Hoffmann, Berthold and Minas, Mark (eds.) , pp. 19–34 (2021)
summary paper bib doi

Summary

Encodings of term rewriting systems (TRSs) into graph rewriting systems usually lose global termination, meaning the encodings do not terminate on all graphs. A typical encoding of the terminating TRS rule a(b(x)) -> b(a(x)), for example, may be indefinitely applicable along a cycle of a's and b's. Recently, we introduced PBPO+, a graph rewriting formalism in which rules employ a type graph to specify transformations and control rule applicability. In the present paper, we show that PBPO+ allows for a natural encoding of linear TRS rules that preserves termination globally. This result is a step towards modeling other rewriting formalisms, such as lambda calculus and higher order rewriting, using graph rewriting in a way that preserves properties like termination and confluence. We moreover expect that the encoding can serve as a guide for lifting TRS termination methods to PBPO+ rewriting.
Bibtex
```
@inproceedings{graph:termination:linear:2021,
  author = {Overbeek, Roy and Endrullis, J{\"{o}}rg},
  editor = {Hoffmann, Berthold and Minas, Mark},
  title = {From Linear Term Rewriting to Graph Rewriting with Preservation of
                    Termination},
  booktitle = {Proceedings Twelfth International Workshop on Graph Computational
                    Models, GCM@STAF 2021, Online, 22nd June 2021},
  series = {{EPTCS}},
  volume = {350},
  pages = {19--34},
  year = {2021},
  url = {https://doi.org/10.4204/EPTCS.350.2},
  doi = {10.4204/EPTCS.350.2},
  biburl = {https://dblp.org/rec/journals/corr/abs-2106-13826.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  keywords = {rewriting, termination},
  type = {workshop}
}
```
Digital Object Identifier
```
10.4204/EPTCS.350.2
```

2013

SAT Compilation for Termination Proofs via Semantic Labelling

Alexander Bau, Jörg Endrullis, and Johannes Waldmann

In: Proc. Workshop on Termination (WST 2007) (2013)

paper bib

Bibtex

@inproceedings{termination:sat:compilation:2014,
  author = {Bau, Alexander and Endrullis, J\"{o}rg and Waldmann, Johannes},
  title = {{SAT compilation for Termination Proofs via Semantic Labelling}},
  booktitle = {Proc.\ Workshop on Termination (WST~2007)},
  year = {2013},
  keywords = {rewriting, termination},
  type = {workshop}
}

Digital Object Identifier

2007

Root Stabilisation Using Dependency Pairs

Jörg Endrullis, and Jeroen Ketema

In: Proc. Workshop on Termination (WST 2007) , pp. 17–21 (2007)

paper bib

Bibtex

@inproceedings{termination:root:2007,
  author = {Endrullis, J\"{o}rg and Ketema, Jeroen},
  title = {{Root Stabilisation Using Dependency Pairs}},
  booktitle = {Proc.\ Workshop on Termination (WST~2007)},
  pages = {17--21},
  year = {2007},
  keywords = {rewriting, infinitary rewriting, termination},
  type = {workshop}
}

Digital Object Identifier

2006

Decomposing Terminating Rewrite Relations
Jörg Endrullis, Dieter Hofbauer, and Johannes Waldmann
In: Proc. Workshop on Termination (WST 2006) , pp. 39–43 (2006)
summary paper bib
Summary

In this paper we are concerned with automatically proving termination of string rewriting systems (or word rewriting systems). We introduce an efficient technique for constructing automata that serve as certificates of match-boundedness, and thereby termination. Previously constructions have either been inefficient or incomplete:
- Match-Bounded String Rewriting Systems by Alfons Geser, Dieter Hofbauer and Johannes Waldmann. The construction in this paper is complete but very inefficient.
- On tree automata that certify termination of left-linear term rewriting systems by Alfons Geser, Dieter Hofbauer, Johannes Waldmann and Hans Zantema. The construction in this paper is efficient but incomplete.
See research for an overview of my research on termination.
Bibtex
```
@inproceedings{termination:matchbounds:2006,
  author = {Endrullis, J\"{o}rg and Hofbauer, Dieter and Waldmann, Johannes},
  title = {{Decomposing Terminating Rewrite Relations}},
  booktitle = {Proc.\ Workshop on Termination (WST~2006)},
  pages = {39--43},
  year = {2006},
  keywords = {rewriting, termination, automata},
  type = {workshop}
}
```
Digital Object Identifier