9 Search Results for "Rehof, Jakob"

Document
DOI: 10.4230/LIPIcs.FSCD.2022.14
Restricting Tree Grammars with Term Rewriting

Authors: Jan Bessai, Lukasz Czajka, Felix Laarmann, and Jakob Rehof

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
We investigate the problem of enumerating all terms generated by a tree-grammar which are also in normal form with respect to a set of directed equations (rewriting relation). To this end we show that deciding emptiness and finiteness of the resulting set is EXPTIME-complete. The emptiness result is inspired by a prior result by Comon and Jacquemard on ground reducibility. The finiteness result is based on modification of pumping arguments used by Comon and Jacquemard. We highlight practical applications and limitations. We provide and evaluate a prototype implementation. Limitations are somewhat surprising in that, while deciding emptiness and finiteness is EXPTIME-complete for linear and nonlinear rewrite relations, the linear case is practically feasible while the nonlinear case is infeasible, even for a trivially small example. The algorithms provided for the linear case also improve on prior practical results by Kallat et al.
Cite as

Jan Bessai, Lukasz Czajka, Felix Laarmann, and Jakob Rehof. Restricting Tree Grammars with Term Rewriting. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bessai_et_al:LIPIcs.FSCD.2022.14,
  author =	{Bessai, Jan and Czajka, Lukasz and Laarmann, Felix and Rehof, Jakob},
  title =	{{Restricting Tree Grammars with Term Rewriting}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.14},
  URN =		{urn:nbn:de:0030-drops-162953},
  doi =		{10.4230/LIPIcs.FSCD.2022.14},
  annote =	{Keywords: tree automata, tree grammar, term rewriting, normalization, emptiness, finiteness}
}
Document
DOI: 10.4230/DagRep.9.9.66
Data Ecosystems: Sovereign Data Exchange among Organizations (Dagstuhl Seminar 19391)

Authors: Cinzia Cappiello, Avigdor Gal, Matthias Jarke, and Jakob Rehof

Published in: Dagstuhl Reports, Volume 9, Issue 9 (2020)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 19391 ``Data Ecosystems: Sovereign Data Exchange among Organizations''. The goal of the seminar was to bring together people from different disciplines (also outside the computer science area), in order to identify (i) a set of research challenges for the future development of data ecosystems and a catalogue of major approaches relevant to the field and (ii) a set of developed use cases of particular interest to the further development of data ecosystems. Towards the objectives, the seminar included tutorials, invited talks, presentations of open problems, working groups. This report presents the most relevant findings and contributions.
Cite as

Cinzia Cappiello, Avigdor Gal, Matthias Jarke, and Jakob Rehof. Data Ecosystems: Sovereign Data Exchange among Organizations (Dagstuhl Seminar 19391). In Dagstuhl Reports, Volume 9, Issue 9, pp. 66-134, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{cappiello_et_al:DagRep.9.9.66,
  author =	{Cappiello, Cinzia and Gal, Avigdor and Jarke, Matthias and Rehof, Jakob},
  title =	{{Data Ecosystems: Sovereign Data Exchange among Organizations (Dagstuhl Seminar 19391)}},
  pages =	{66--134},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{9},
  number =	{9},
  editor =	{Cappiello, Cinzia and Gal, Avigdor and Jarke, Matthias and Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.9.9.66},
  URN =		{urn:nbn:de:0030-drops-118450},
  doi =		{10.4230/DagRep.9.9.66},
  annote =	{Keywords: Data sovereignty, Data ecosystems, Business models, Data integration, Ethics}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2018.2
A Simpler Undecidability Proof for System F Inhabitation

Authors: Andrej Dudenhefner and Jakob Rehof

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
Provability in the intuitionistic second-order propositional logic (resp. inhabitation in the polymorphic lambda-calculus) was shown by Löb to be undecidable in 1976. Since the original proof is heavily condensed, Arts in collaboration with Dekkers provided a fully unfolded argument in 1992 spanning approximately fifty pages. Later in 1997, Urzyczyn developed a different, syntax oriented proof. Each of the above approaches embeds (an undecidable fragment of) first-order predicate logic into second-order propositional logic. In this work, we develop a simpler undecidability proof by reduction from solvability of Diophantine equations (is there an integer solution to P(x_1, ..., x_n) = 0 where P is a polynomial with integer coefficients?). Compared to the previous approaches, the given reduction is more accessible for formalization and more comprehensible for didactic purposes. Additionally, we formalize soundness and completeness of the reduction in the Coq proof assistant under the banner of "type theory inside type theory".
Cite as

Andrej Dudenhefner and Jakob Rehof. A Simpler Undecidability Proof for System F Inhabitation. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 2:1-2:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2018.2,
  author =	{Dudenhefner, Andrej and Rehof, Jakob},
  title =	{{A Simpler Undecidability Proof for System F Inhabitation}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{2:1--2:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.2},
  URN =		{urn:nbn:de:0030-drops-114061},
  doi =		{10.4230/LIPIcs.TYPES.2018.2},
  annote =	{Keywords: System F, Lambda Calculus, Inhabitation, Propositional Logic, Provability, Undecidability, Coq, Formalization}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2017.2
Lower End of the Linial-Post Spectrum

Authors: Andrej Dudenhefner and Jakob Rehof

Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)

Abstract
We show that recognizing axiomatizations of the Hilbert-style calculus containing only the axiom a -> (b -> a) is undecidable (a reduction from the Post correspondence problem is formalized in the Lean theorem prover). Interestingly, the problem remains undecidable considering only axioms which, when seen as simple types, are principal for some lambda-terms in beta-normal form. This problem is closely related to type-based composition synthesis, i.e. finding a composition of given building blocks (typed terms) satisfying a desired specification (goal type). Contrary to the above result, axiomatizations of the Hilbert-style calculus containing only the axiom a -> (b -> b) are recognizable in linear time.
Cite as

Andrej Dudenhefner and Jakob Rehof. Lower End of the Linial-Post Spectrum. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 2:1-2:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.TYPES.2017.2,
  author =	{Dudenhefner, Andrej and Rehof, Jakob},
  title =	{{Lower End of the Linial-Post Spectrum}},
  booktitle =	{23rd International Conference on Types for Proofs and Programs (TYPES 2017)},
  pages =	{2:1--2:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-071-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{104},
  editor =	{Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.2},
  URN =		{urn:nbn:de:0030-drops-100503},
  doi =		{10.4230/LIPIcs.TYPES.2017.2},
  annote =	{Keywords: combinatory logic, lambda calculus, type theory, simple types, inhabitation, principal type}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.15
The Complexity of Principal Inhabitation

Authors: Andrej Dudenhefner and Jakob Rehof

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

Abstract
It is shown that in the simply typed lambda-calculus the following decision problem of principal inhabitation is Pspace-complete: Given a simple type tau, is there a lambda-term N in beta-normal form such that tau is the principal type of N? While a Ben-Yelles style algorithm was presented by Broda and Damas in 1999 to count normal principal inhabitants (thereby answering a question posed by Hindley), it does not induce a polynomial space upper bound for principal inhabitation. Further, the standard construction of the polynomial space lower bound for simple type inhabitation does not carry over immediately. We present a polynomial space bounded decision procedure based on a characterization of principal inhabitation using path derivation systems over subformulae of the input type, which does not require candidate inhabitants to be constructed explicitly. The lower bound is shown by reducing a restriction of simple type inhabitation to principal inhabitation.
Cite as

Andrej Dudenhefner and Jakob Rehof. The Complexity of Principal Inhabitation. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2017.15,
  author =	{Dudenhefner, Andrej and Rehof, Jakob},
  title =	{{The Complexity of Principal Inhabitation}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{15:1--15:14},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.15},
  URN =		{urn:nbn:de:0030-drops-77359},
  doi =		{10.4230/LIPIcs.FSCD.2017.15},
  annote =	{Keywords: Lambda Calculus, Type Theory, Simple Types, Inhabitation, Principal Type, Complexity}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.19
The Intersection Type Unification Problem

Authors: Andrej Dudenhefner, Moritz Martens, and Jakob Rehof

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
The intersection type unification problem is an important component in proof search related to several natural decision problems in intersection type systems. It is unknown and remains open whether the unification problem is decidable. We give the first nontrivial lower bound for the problem by showing (our main result) that it is exponential time hard. Furthermore, we show that this holds even under rank 1 solutions (substitutions whose codomains are restricted to contain rank 1 types). In addition, we provide a fixed-parameter intractability result for intersection type matching (one-sided unification), which is known to be NP-complete. We place the intersection type unification problem in the context of unification theory. The equational theory of intersection types can be presented as an algebraic theory with an ACI (associative, commutative, and idempotent) operator (intersection type) combined with distributivity properties with respect to a second operator (function type). Although the problem is algebraically natural and interesting, it appears to occupy a hitherto unstudied place in the theory of unification, and our investigation of the problem suggests that new methods are required to understand the problem. Thus, for the lower bound proof, we were not able to reduce from known results in ACI-unification theory and use game-theoretic methods for two-player tiling games.
Cite as

Andrej Dudenhefner, Moritz Martens, and Jakob Rehof. The Intersection Type Unification Problem. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 19:1-19:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dudenhefner_et_al:LIPIcs.FSCD.2016.19,
  author =	{Dudenhefner, Andrej and Martens, Moritz and Rehof, Jakob},
  title =	{{The Intersection Type Unification Problem}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{19:1--19:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.19},
  URN =		{urn:nbn:de:0030-drops-59955},
  doi =		{10.4230/LIPIcs.FSCD.2016.19},
  annote =	{Keywords: Intersection Type, Equational Theory, Unification, Tiling, Complexity}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.76
Mixin Composition Synthesis Based on Intersection Types

Authors: Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de’Liguoro, and Jakob Rehof

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
We present a method for synthesizing compositions of mixins using type inhabitation in intersection types. First, recursively defined classes and mixins, which are functions over classes, are expressed as terms in a lambda calculus with records. Intersection types with records and record-merge are used to assign meaningful types to these terms without resorting to recursive types. Second, typed terms are translated to a repository of typed combinators. We show a relation between record types with record-merge and intersection types with constructors. This relation is used to prove soundness and partial completeness of the translation with respect to mixin composition synthesis. Furthermore, we demonstrate how a translated repository and goal type can be used as input to an existing framework for composition synthesis in bounded combinatory logic via type inhabitation. The computed result corresponds to a mixin composition typed by the goal type.
Cite as

Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de’Liguoro, and Jakob Rehof. Mixin Composition Synthesis Based on Intersection Types. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 76-91, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bessai_et_al:LIPIcs.TLCA.2015.76,
  author =	{Bessai, Jan and Dudenhefner, Andrej and D\"{u}dder, Boris and Chen, Tzu-Chun and de’Liguoro, Ugo and Rehof, Jakob},
  title =	{{Mixin Composition Synthesis Based on Intersection Types}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{76--91},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.76},
  URN =		{urn:nbn:de:0030-drops-51563},
  doi =		{10.4230/LIPIcs.TLCA.2015.76},
  annote =	{Keywords: Record Calculus, Combinatory Logic, Type Inhabitation, Mixin, Intersection Type}
}
Document
DOI: 10.4230/DagRep.4.6.29
Design and Synthesis from Components (Dagstuhl Seminar 14232)

Authors: Jakob Rehof and Moshe Y. Vardi

Published in: Dagstuhl Reports, Volume 4, Issue 6 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14232 "Design and Synthesis from Components" which took place from June 1st to June 6th, 2014. The seminar aimed at bringing together researchers from the component-oriented design community, researchers working on interface theories, and researchers working in synthesis, in order to explore the use of component- and interface design in program synthesis. The seminar program consisted of 6 tutorial talks (1 hour) and 16 contributed talks (30 mins) as well as joint discussion sessions. This report documents the abstracts of the talks as well as summaries of discussion sessions.
Cite as

Jakob Rehof and Moshe Y. Vardi. Design and Synthesis from Components (Dagstuhl Seminar 14232). In Dagstuhl Reports, Volume 4, Issue 6, pp. 29-47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{rehof_et_al:DagRep.4.6.29,
  author =	{Rehof, Jakob and Vardi, Moshe Y.},
  title =	{{Design and Synthesis from Components (Dagstuhl Seminar 14232)}},
  pages =	{29--47},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{6},
  editor =	{Rehof, Jakob and Vardi, Moshe Y.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.4.6.29},
  URN =		{urn:nbn:de:0030-drops-46839},
  doi =		{10.4230/DagRep.4.6.29},
  annote =	{Keywords: Component design, Component-based synthesis}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.243
Bounded Combinatory Logic

Authors: Boris Düdder, Moritz Martens, Jakob Rehof, and Pawel Urzyczyn

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
In combinatory logic one usually assumes a fixed set of basic combinators (axiom schemes), usually K and S. In this setting the set of provable formulas (inhabited types) is PSPACE-complete in simple types and undecidable in intersection types. When arbitrary sets of axiom schemes are considered, the inhabitation problem is undecidable even in simple types (this is known as Linial-Post theorem). k-bounded combinatory logic with intersection types arises from combinatory logic by imposing the bound k on the depth of types (formulae) which may be substituted for type variables in axiom schemes. We consider the inhabitation (provability) problem for k-bounded combinatory logic: Given an arbitrary set of typed combinators and a type tau, is there a combinatory term of type tau in k-bounded combinatory logic? Our main result is that the problem is (k+2)-EXPTIME complete for k-bounded combinatory logic with intersection types, for every fixed k (and hence non-elementary when k is a parameter). We also show that the problem is EXPTIME-complete for simple types, for all k. Theoretically, our results give new insight into the expressive power of intersection types. From an application perspective, our results are useful as a foundation for composition synthesis based on combinatory logic.
Cite as

Boris Düdder, Moritz Martens, Jakob Rehof, and Pawel Urzyczyn. Bounded Combinatory Logic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 243-258, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{dudder_et_al:LIPIcs.CSL.2012.243,
  author =	{D\"{u}dder, Boris and Martens, Moritz and Rehof, Jakob and Urzyczyn, Pawel},
  title =	{{Bounded Combinatory Logic}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{243--258},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.243},
  URN =		{urn:nbn:de:0030-drops-36763},
  doi =		{10.4230/LIPIcs.CSL.2012.243},
  annote =	{Keywords: Intersection types, Inhabitation, Composition synthesis}
}
  • Refine by Author
  • 9 Rehof, Jakob
  • 5 Dudenhefner, Andrej
  • 2 Bessai, Jan
  • 2 Düdder, Boris
  • 2 Martens, Moritz
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Automata extensions
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Proof theory
  • 1 Theory of computation → Tree languages
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 3 Inhabitation
  • 2 Complexity
  • 2 Intersection Type
  • 2 Lambda Calculus
  • 1 Business models
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 2 2019
  • 1 2012
  • 1 2014
  • 1 2015
  • 1 2016
  • Show More...

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