Search Results

Documents authored by Charatonik, Witold

Document
DOI: 10.4230/LIPIcs.ITP.2022.7
The Zoo of Lambda-Calculus Reduction Strategies, And Coq

Authors: Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
We present a generic framework for the specification and reasoning about reduction strategies in the lambda calculus, representable as sets of term decompositions. It is provided as a Coq formalization that features a novel format of phased strategies. It facilitates concise description and algebraic reasoning about properties of reduction strategies. The formalization accommodates many well-known strategies, both weak and strong, such as call by name, call by value, head reduction, normal order, full β-reduction, etc. We illustrate the use of the framework as a tool to inspect and categorize the "zoo" of existing strategies, as well as to discover and study new ones with particular properties.
Cite as

Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab. The Zoo of Lambda-Calculus Reduction Strategies, And Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{biernacka_et_al:LIPIcs.ITP.2022.7,
  author =	{Biernacka, Ma{\l}gorzata and Charatonik, Witold and Drab, Tomasz},
  title =	{{The Zoo of Lambda-Calculus Reduction Strategies, And Coq}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.7},
  URN =		{urn:nbn:de:0030-drops-167165},
  doi =		{10.4230/LIPIcs.ITP.2022.7},
  annote =	{Keywords: Lambda calculus, Reduction strategies, Coq}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.8
Deriving an Abstract Machine for Strong Call by Need

Authors: Małgorzata Biernacka and Witold Charatonik

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
Strong call by need is a reduction strategy for computing strong normal forms in the lambda calculus, where terms are fully normalized inside the bodies of lambda abstractions and open terms are allowed. As typical for a call-by-need strategy, the arguments of a function call are evaluated at most once, only when they are needed. This strategy has been introduced recently by Balabonski et al., who proved it complete with respect to full beta-reduction and conservative over weak call by need. We show a novel reduction semantics and the first abstract machine for the strong call-by-need strategy. The reduction semantics incorporates syntactic distinction between strict and non-strict let constructs and is geared towards an efficient implementation. It has been defined within the framework of generalized refocusing, i.e., a generic method that allows to go from a reduction semantics instrumented with context kinds to the corresponding abstract machine; the machine is thus correct by construction. The format of the semantics that we use makes it explicit that strong call by need is an example of a hybrid strategy with an infinite number of substrategies.
Cite as

Małgorzata Biernacka and Witold Charatonik. Deriving an Abstract Machine for Strong Call by Need. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{biernacka_et_al:LIPIcs.FSCD.2019.8,
  author =	{Biernacka, Ma{\l}gorzata and Charatonik, Witold},
  title =	{{Deriving an Abstract Machine for Strong Call by Need}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.8},
  URN =		{urn:nbn:de:0030-drops-105159},
  doi =		{10.4230/LIPIcs.FSCD.2019.8},
  annote =	{Keywords: abstract machines, reduction semantics}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.12
Modulo Counting on Words and Trees

Authors: Bartosz Bednarczyk and Witold Charatonik

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a technique for deciding the satisfiability problem. In the case of words this gives a new proof of EXPSPACE upper bound, and in the case of trees it gives a 2EXPTIME algorithm. This algorithm is optimal: we prove a matching lower bound by a generic reduction from alternating Turing machines working in exponential space; the reduction involves a development of a new version of tiling games.
Cite as

Bartosz Bednarczyk and Witold Charatonik. Modulo Counting on Words and Trees. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bednarczyk_et_al:LIPIcs.FSTTCS.2017.12,
  author =	{Bednarczyk, Bartosz and Charatonik, Witold},
  title =	{{Modulo Counting on Words and Trees}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.12},
  URN =		{urn:nbn:de:0030-drops-84083},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.12},
  annote =	{Keywords: satisfiability, trees, words, two-variable logic, modulo quantifiers}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.10
Generalized Refocusing: From Hybrid Strategies to Abstract Machines

Authors: Malgorzata Biernacka, Witold Charatonik, and Klara Zielinska

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

Abstract
We present a generalization of the refocusing procedure that provides a generic method for deriving an abstract machine from a specification of a reduction semantics satisfying simple initial conditions. The proposed generalization is applicable to a class of reduction semantics encoding hybrid strategies as well as uniform strategies handled by the original refocusing method. The resulting machine is proved to correctly trace (i.e., bisimulate in smaller steps) the input reduction semantics. The procedure and the correctness proofs have been formalized in the Coq proof assistant.
Cite as

Malgorzata Biernacka, Witold Charatonik, and Klara Zielinska. Generalized Refocusing: From Hybrid Strategies to Abstract Machines. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{biernacka_et_al:LIPIcs.FSCD.2017.10,
  author =	{Biernacka, Malgorzata and Charatonik, Witold and Zielinska, Klara},
  title =	{{Generalized Refocusing: From Hybrid Strategies to Abstract Machines}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{10:1--10:17},
  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.10},
  URN =		{urn:nbn:de:0030-drops-77188},
  doi =		{10.4230/LIPIcs.FSCD.2017.10},
  annote =	{Keywords: reduction semantics, abstract machines, formal verification, Coq}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.11
Extending Two-Variable Logic on Trees

Authors: Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieronski

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

Abstract
The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.
Cite as

Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieronski. Extending Two-Variable Logic on Trees. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bednarczyk_et_al:LIPIcs.CSL.2017.11,
  author =	{Bednarczyk, Bartosz and Charatonik, Witold and Kieronski, Emanuel},
  title =	{{Extending Two-Variable Logic on Trees}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{11:1--11:20},
  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.11},
  URN =		{urn:nbn:de:0030-drops-76794},
  doi =		{10.4230/LIPIcs.CSL.2017.11},
  annote =	{Keywords: two-variable logic, trees, satisfiability, expressivity, counting quantifiers}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.631
Two-variable Logic with Counting and a Linear Order

Authors: Witold Charatonik and Piotr Witkowski

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
We study the finite satisfiability problem for the two-variable fragment of the first-order logic extended with counting quantifiers (C2) and interpreted over linearly ordered structures. We show that the problem is undecidable in the case of two linear orders (in presence of two other binary symbols). In the case of one linear order it is NEXPTIME-complete, even in presence of the successor relation. Surprisingly, the complexity of the problem explodes when we add one binary symbol more: C2 with one linear order and its successor, in presence of other binary predicate symbols, is decidable, but it is as expressive (and as complex) as Vector Addition Systems.
Cite as

Witold Charatonik and Piotr Witkowski. Two-variable Logic with Counting and a Linear Order. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 631-647, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{charatonik_et_al:LIPIcs.CSL.2015.631,
  author =	{Charatonik, Witold and Witkowski, Piotr},
  title =	{{Two-variable Logic with Counting and a Linear Order}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{631--647},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.631},
  URN =		{urn:nbn:de:0030-drops-54436},
  doi =		{10.4230/LIPIcs.CSL.2015.631},
  annote =	{Keywords: Two-variable logic, counting quantifiers, linear order, satisfiability, complexity}
}
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