Search Results

Documents authored by Bahr, Patrick

Document
DOI: 10.4230/LIPIcs.FSCD.2018.8
Strict Ideal Completions of the Lambda Calculus

Authors: Patrick Bahr

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
The infinitary lambda calculi pioneered by Kennaway et al. extend the basic lambda calculus by metric completion to infinite terms and reductions. Depending on the chosen metric, the resulting infinitary calculi exhibit different notions of strictness. To obtain infinitary normalisation and infinitary confluence properties for these calculi, Kennaway et al. extend beta-reduction with infinitely many `bot-rules', which contract meaningless terms directly to bot. Three of the resulting Böhm reduction calculi have unique infinitary normal forms corresponding to Böhm-like trees. In this paper we develop a corresponding theory of infinitary lambda calculi based on ideal completion instead of metric completion. We show that each of our calculi conservatively extends the corresponding metric-based calculus. Three of our calculi are infinitarily normalising and confluent; their unique infinitary normal forms are exactly the Böhm-like trees of the corresponding metric-based calculi. Our calculi dispense with the infinitely many bot-rules of the metric-based calculi. The fully non-strict calculus (called 111) consists of only beta-reduction, while the other two calculi (called 001 and 101) require two additional rules that precisely state their strictness properties: lambda x.bot -> bot (for 001) and bot M -> bot (for 001 and 101).
Cite as

Patrick Bahr. Strict Ideal Completions of the Lambda Calculus. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bahr:LIPIcs.FSCD.2018.8,
  author =	{Bahr, Patrick},
  title =	{{Strict Ideal Completions of the Lambda Calculus}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.8},
  URN =		{urn:nbn:de:0030-drops-91787},
  doi =		{10.4230/LIPIcs.FSCD.2018.8},
  annote =	{Keywords: lambda calculus, infinitary rewriting, B\"{o}hm trees, meaningless terms, confluence}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.8
Böhm Reduction in Infinitary Term Graph Rewriting Systems

Authors: Patrick Bahr

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
The confluence properties of lambda calculus and orthogonal term rewriting do not generalise to the corresponding infinitary calculi. In order to recover the confluence property in a meaningful way, Kennaway et al. introduced Böhm reduction, which extends the ordinary reduction relation so that "meaningless terms" can be contracted to a fresh constant "bottom". In previous work, we have established that Böhm reduction can be instead characterised by a different mode of convergences of transfinite reductions that is based on a partial order structure instead of a metric space. In this paper, we develop a corresponding theory of Böhm reduction for term graphs. Our main result is that partial order convergence in a term graph rewriting system can be truthfully and faithfully simulated by metric convergence in the Böhm extension of the system. To prove this result we generalise the notion of residuals and projections to the setting of infinitary term graph rewriting. As ancillary results we prove the infinitary strip lemma and the compression property, both for partial order and metric convergence.
Cite as

Patrick Bahr. Böhm Reduction in Infinitary Term Graph Rewriting Systems. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bahr:LIPIcs.FSCD.2017.8,
  author =	{Bahr, Patrick},
  title =	{{B\"{o}hm Reduction in Infinitary Term Graph Rewriting Systems}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.8},
  URN =		{urn:nbn:de:0030-drops-77275},
  doi =		{10.4230/LIPIcs.FSCD.2017.8},
  annote =	{Keywords: infinitary rewriting, term graphs, B\"{o}hm trees}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.69
Infinitary Term Graph Rewriting is Simple, Sound and Complete

Authors: Patrick Bahr

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Based on a simple metric and a simple partial order on term graphs, we develop two infinitary calculi of term graph rewriting. We show that, similarly to infinitary term rewriting, the partial order formalisation yields a conservative extension of the metric formalisation of the calculus. By showing that the resulting calculi simulate the corresponding well-established infinitary calculi of term rewriting in a sound and complete manner, we argue for the appropriateness of our approach to capture the notion of infinitary term graph rewriting.
Cite as

Patrick Bahr. Infinitary Term Graph Rewriting is Simple, Sound and Complete. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 69-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bahr:LIPIcs.RTA.2012.69,
  author =	{Bahr, Patrick},
  title =	{{Infinitary Term Graph Rewriting is Simple, Sound and Complete}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{69--84},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.69},
  URN =		{urn:nbn:de:0030-drops-34857},
  doi =		{10.4230/LIPIcs.RTA.2012.69},
  annote =	{Keywords: term graphs, infinitary rewriting}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.139
Modes of Convergence for Term Graph Rewriting

Authors: Patrick Bahr

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
Term graph rewriting provides a simple mechanism to finitely represent restricted forms of infinitary term rewriting. The correspondence between infinitary term rewriting and term graph rewriting has been studied to some extent. However, this endeavour is impaired by the lack of an appropriate counterpart of infinitary rewriting on the side of term graphs. We aim to fill this gap by devising two modes of convergence based on a partial order resp. a metric on term graphs. The thus obtained structures generalise corresponding modes of convergence that are usually studied in infinitary term rewriting. We argue that this yields a common framework in which both term rewriting and term graph rewriting can be studied. In order to substantiate our claim, we compare convergence on term graphs and on terms. In particular, we show that the resulting infinitary calculi of term graph rewriting exhibit the same correspondence as we know it from term rewriting: Convergence via the partial order is a conservative extension of the metric convergence.
Cite as

Patrick Bahr. Modes of Convergence for Term Graph Rewriting. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 139-154, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bahr:LIPIcs.RTA.2011.139,
  author =	{Bahr, Patrick},
  title =	{{Modes of Convergence for Term Graph Rewriting}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{139--154},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.139},
  URN =		{urn:nbn:de:0030-drops-31131},
  doi =		{10.4230/LIPIcs.RTA.2011.139},
  annote =	{Keywords: term graphs, partial order, metric, infinitary rewriting, graph rewriting}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.49
Abstract Models of Transfinite Reductions

Authors: Patrick Bahr

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
We investigate transfinite reductions in abstract reduction systems. To this end, we study two abstract models for transfinite reductions: a metric model generalising the usual metric approach to infinitary term rewriting and a novel partial order model. For both models we distinguish between a weak and a strong variant of convergence as known from infinitary term rewriting. Furthermore, we introduce an axiomatic model of reductions that is general enough to cover all of these models of transfinite reductions as well as the ordinary model of finite reductions. It is shown that, in this unifying axiomatic model, many basic relations between termination and confluence properties known from finite reductions still hold. The introduced models are applied to term rewriting but also to term graph rewriting. We can show that for both term rewriting as well as for term graph rewriting the partial order model forms a conservative extension to the metric model.
Cite as

Patrick Bahr. Abstract Models of Transfinite Reductions. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 49-66, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bahr:LIPIcs.RTA.2010.49,
  author =	{Bahr, Patrick},
  title =	{{Abstract Models of Transfinite Reductions}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{49--66},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.49},
  URN =		{urn:nbn:de:0030-drops-26445},
  doi =		{10.4230/LIPIcs.RTA.2010.49},
  annote =	{Keywords: Infinitary rewriting, metric, partial order, abstract reduction system, axiomatic, term rewriting, graph rewriting}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.67
Partial Order Infinitary Term Rewriting and Böhm Trees

Authors: Patrick Bahr

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
We investigate an alternative model of infinitary term rewriting. Instead of a metric, a partial order on terms is employed to formalise (strong) convergence. We compare this partial order convergence of orthogonal term rewriting systems to the usual metric convergence of the corresponding B{"o}hm extensions. The B{"o}hm extension of a term rewriting system contains additional rules to equate so-called root-active terms. The core result we present is that reachability w.r.t. partial order convergence coincides with reachability w.r.t. metric convergence in the B{"o}hm extension. This result is used to show that, unlike in the metric model, orthogonal systems are infinitarily confluent and infinitarily normalising in the partial order model. Moreover, we obtain, as in the metric model, a compression lemma. A corollary of this lemma is that reachability w.r.t. partial order convergence is a conservative extension of reachability w.r.t. metric convergence.
Cite as

Patrick Bahr. Partial Order Infinitary Term Rewriting and Böhm Trees. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 67-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bahr:LIPIcs.RTA.2010.67,
  author =	{Bahr, Patrick},
  title =	{{Partial Order Infinitary Term Rewriting and B\"{o}hm Trees}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{67--84},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.67},
  URN =		{urn:nbn:de:0030-drops-26455},
  doi =		{10.4230/LIPIcs.RTA.2010.67},
  annote =	{Keywords: Infinitary term rewriting, B\"{o}hm trees, partial order, confluence, normalisation}
}
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