-
Extension property for partial automorphisms of the $n$-partite and semigeneric tournaments
Authors:
Jan Hubička,
Colin Jahel,
Matěj Konečný,
Marcin Sabok
Abstract:
We present a proof of the extension property for partial automorphisms (EPPA) for classes of finite $n$-partite tournaments for $n \in \{2,3,\ldots,ω\}$, and for the class of finite semigeneric tournaments. We also prove that the generic $ω$-partite tournament and the generic semigeneric tournament have ample generics.
We present a proof of the extension property for partial automorphisms (EPPA) for classes of finite $n$-partite tournaments for $n \in \{2,3,\ldots,ω\}$, and for the class of finite semigeneric tournaments. We also prove that the generic $ω$-partite tournament and the generic semigeneric tournament have ample generics.
△ Less
Submitted 22 January, 2024;
originally announced January 2024.
-
EPPA numbers of graphs
Authors:
David Bradley-Williams,
Peter J. Cameron,
Jan Hubička,
Matěj Konečný
Abstract:
If $G$ is a graph, $A$ and $B$ its induced subgraphs, and $f\colon A\to B$ an isomorphism, we say that $f$ is a partial automorphism of $G$. In 1992, Hrushovski proved that graphs have the extension property for partial automorphisms (EPPA, also called the Hrushovski property), that is, for every finite graph $G$ there is a finite graph $H$, its EPPA-witness, such that $G$ is an induced subgraph o…
▽ More
If $G$ is a graph, $A$ and $B$ its induced subgraphs, and $f\colon A\to B$ an isomorphism, we say that $f$ is a partial automorphism of $G$. In 1992, Hrushovski proved that graphs have the extension property for partial automorphisms (EPPA, also called the Hrushovski property), that is, for every finite graph $G$ there is a finite graph $H$, its EPPA-witness, such that $G$ is an induced subgraph of $H$ and every partial automorphism of $G$ extends to an automorphism of $H$.
The EPPA number of a graph $G$, denoted by $\mathop{\mathrm{eppa}}\nolimits(G)$, is the smallest number of vertices of an EPPA-witness for $G$, and we put $\mathop{\mathrm{eppa}}\nolimits(n) = \max\{\mathop{\mathrm{eppa}}\nolimits(G) : \lvert G\rvert = n\}$. In this note we review the state of the area, prove several lower bounds (in particular, we show that $\mathop{\mathrm{eppa}}\nolimits(n)\geq \frac{2^n}{\sqrt{n}}$, thereby identifying the correct base of the exponential) and pose many open questions. We also briefly discuss EPPA numbers of hypergraphs, directed graphs, and $K_k$-free graphs.
△ Less
Submitted 10 December, 2023; v1 submitted 14 November, 2023;
originally announced November 2023.
-
Ramsey theorem for trees with successor operation
Authors:
Martin Balko,
David Chodounský,
Natasha Dobrinen,
Jan Hubička,
Matěj Konečný,
Jaroslav Nešetřil,
Andy Zucker
Abstract:
We prove a general Ramsey theorem for trees with a successor operation. This theorem is a common generalization of the Carlson-Simpson Theorem and the Milliken Tree Theorem for regularly branching trees.
Our theorem has a number of applications both in finite and infinite combinatorics. For example, we give a short proof of the unrestricted Nešetřil-Rödl theorem, and we recover the Graham-Rothsc…
▽ More
We prove a general Ramsey theorem for trees with a successor operation. This theorem is a common generalization of the Carlson-Simpson Theorem and the Milliken Tree Theorem for regularly branching trees.
Our theorem has a number of applications both in finite and infinite combinatorics. For example, we give a short proof of the unrestricted Nešetřil-Rödl theorem, and we recover the Graham-Rothschild theorem. Our original motivation came from the study of big Ramsey degrees - various trees used in the study can be viewed as trees with a successor operation. To illustrate this, we give a non-forcing proof of a theorem of Zucker on big Ramsey degrees.
△ Less
Submitted 12 November, 2023;
originally announced November 2023.
-
Big Ramsey degrees in the metric setting
Authors:
Tristan Bice,
Noé de Rancourt,
Jan Hubička,
Matěj Konečný
Abstract:
Oscillation stability is an important concept in Banach space theory which happens to be closely connected to discrete Ramsey theory. For example, Gowers proved oscillation stability for the Banach space $c_0$ using his now famous Ramsey theorem for $\mathrm{FIN}_k$ as the key ingredient. We develop the theory behind this connection and introduce the notion of compact big Ramsey degrees, extending…
▽ More
Oscillation stability is an important concept in Banach space theory which happens to be closely connected to discrete Ramsey theory. For example, Gowers proved oscillation stability for the Banach space $c_0$ using his now famous Ramsey theorem for $\mathrm{FIN}_k$ as the key ingredient. We develop the theory behind this connection and introduce the notion of compact big Ramsey degrees, extending the theory of (discrete) big Ramsey degrees. We then prove existence of compact big Ramsey degrees for the Banach space $\ell_\infty$ and the Urysohn sphere, with an explicit characterization in the case of $\ell_\infty$.
△ Less
Submitted 25 March, 2023;
originally announced March 2023.
-
Type-respecting amalgamation and big Ramsey degrees
Authors:
Andrés Aranda,
Samuel Braunfeld,
David Chodounský,
Jan Hubička,
Matěj Konečný,
Jaroslav Nešetřil,
Andy Zucker
Abstract:
We give an infinitary extension of the Nešetřil-Rödl theorem for category of relational structures with special type-respecting embeddings.
We give an infinitary extension of the Nešetřil-Rödl theorem for category of relational structures with special type-respecting embeddings.
△ Less
Submitted 22 March, 2023;
originally announced March 2023.
-
Characterisation of the big Ramsey degrees of the generic partial order
Authors:
Martin Balko,
David Chodounský,
Natasha Dobrinen,
Jan Hubička,
Matěj Konečný,
Lluis Vena,
Andy Zucker
Abstract:
As a result of 33 intercontinental Zoom calls, we characterise big Ramsey degrees of the generic partial order. This is an infinitary extension of the well known fact that finite partial orders endowed with linear extensions form a Ramsey class (this result was announced by Nešetřil and Rödl in 1984 with first published proof by Paoli, Trotter and Walker in 1985). Towards this, we refine earlier u…
▽ More
As a result of 33 intercontinental Zoom calls, we characterise big Ramsey degrees of the generic partial order. This is an infinitary extension of the well known fact that finite partial orders endowed with linear extensions form a Ramsey class (this result was announced by Nešetřil and Rödl in 1984 with first published proof by Paoli, Trotter and Walker in 1985). Towards this, we refine earlier upper bounds obtained by Hubička based on a new connection of big Ramsey degrees to the Carlson-Simpson theorem and we also introduce a new technique of giving lower bounds using an iterated application of the upper-bound theorem.
△ Less
Submitted 17 June, 2024; v1 submitted 17 March, 2023;
originally announced March 2023.
-
Big Ramsey degrees and infinite languages
Authors:
Samuel Braunfeld,
David Chodounský,
Noé de Rancourt,
Jan Hubička,
Jamal Kawach,
Matěj Konečný
Abstract:
This paper investigates big Ramsey degrees of unrestricted relational structures in (possibly) infinite languages. While significant progress has been made in studying big Ramsey degrees, many classes of structures with finite small Ramsey degrees still lack an understanding of their big Ramsey degrees. We show that if there are only finitely many relations of every arity greater than one, then un…
▽ More
This paper investigates big Ramsey degrees of unrestricted relational structures in (possibly) infinite languages. While significant progress has been made in studying big Ramsey degrees, many classes of structures with finite small Ramsey degrees still lack an understanding of their big Ramsey degrees. We show that if there are only finitely many relations of every arity greater than one, then unrestricted relational structures have finite big Ramsey degrees, and give some evidence that this is tight. This is the first time that finiteness of big Ramsey degrees has been established for an infinite-language random structure. Our results represent an important step towards a better understanding of big Ramsey degrees for structures with relations of arity greater than two.
△ Less
Submitted 14 November, 2023; v1 submitted 30 January, 2023;
originally announced January 2023.
-
Auto-active Verification of Floating-point Programs via Nonlinear Real Provers
Authors:
Junaid Rasheed,
Michal Konečný
Abstract:
We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying programs against tight error bounds featuring common elementary functions. We demonstrate and evaluate our implementation on several examples, yielding the first fully verified SPARK implementations of the sine and square root functions. The process i…
▽ More
We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying programs against tight error bounds featuring common elementary functions. We demonstrate and evaluate our implementation on several examples, yielding the first fully verified SPARK implementations of the sine and square root functions. The process integrates existing tools using a series of transformations and derivations, building on the proving process in SPARK where Why3 produces Verification Conditions (VCs) and tools such as SMT solvers attempt to verify them. We add steps aimed specifically at VCs that contain inequalities with both floating-point operations and exact real functions. PropaFP is our open-source implementation of these steps. The steps include symbolic simplifications, deriving bounds via interval arithmetic, and safely replacing floating-point operations with exact operations, utilizing tools such as FPTaylor or Gappa to bound the compound rounding errors of expressions. Finally, the VCs are passed to provers such as dReal, MetiTarski or LPPaver which attempt to complete the proof or suggest possible counter-examples.
△ Less
Submitted 2 July, 2022;
originally announced July 2022.
-
Extracting efficient exact real number computation from proofs in constructive type theory
Authors:
Michal Konečný,
Sewon Park,
Holger Thies
Abstract:
Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When proving the correctness of an implementation, one can focus solely on the mathematical properties of the problem without thinking about the subtleties of representing real numbers. We propose a new axiomatization of the real…
▽ More
Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When proving the correctness of an implementation, one can focus solely on the mathematical properties of the problem without thinking about the subtleties of representing real numbers. We propose a new axiomatization of the real numbers in a dependent type theory with the goal of extracting certified exact real computation programs from constructive proofs. Our formalization differs from similar approaches, in that we formalize the reals in a conceptually similar way as some mature implementations of exact real computation. Primitive operations on reals can be extracted directly to the corresponding operations in such an implementation, producing more efficient programs. We particularly focus on the formalization of partial and nondeterministic computation, which is essential in exact real computation.
We prove the soundness of our formalization with regards of the standard realizability interpretation from computable analysis and show how to relate our theory to a classical formalization of the reals. We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples. From the examples we have automatically extracted Haskell programs that use the exact real computation framework AERN for efficiently performing exact operations on real numbers. In experiments, the extracted programs behave similarly to native implementations in AERN in terms of running time and memory usage.
△ Less
Submitted 2 February, 2022;
originally announced February 2022.
-
Big Ramsey degrees and forbidden cycles
Authors:
Martin Balko,
David Chodounský,
Jan Hubička,
Matěj Konečný,
Jaroslav Nešetřil,
Lluís Vena
Abstract:
Using the Carlson-Simpson theorem, we give a new general condition for a structure in a finite binary relational language to have finite big Ramsey degrees
Using the Carlson-Simpson theorem, we give a new general condition for a structure in a finite binary relational language to have finite big Ramsey degrees
△ Less
Submitted 25 May, 2021;
originally announced May 2021.
-
Big Ramsey degrees of the generic partial order
Authors:
Martin Balko,
David Chodounský,
Natasha Dobrinen,
Jan Hubička,
Matěj Konečný,
Lluis Vena,
Andy Zucker
Abstract:
As a result of 33 intercontinental Zoom calls, we characterise big Ramsey degrees of the generic partial order in a similar way as Devlin characterised big Ramsey degrees of the generic linear order (the order of rationals).
As a result of 33 intercontinental Zoom calls, we characterise big Ramsey degrees of the generic partial order in a similar way as Devlin characterised big Ramsey degrees of the generic linear order (the order of rationals).
△ Less
Submitted 21 May, 2021;
originally announced May 2021.
-
Big Ramsey degrees of 3-uniform hypergraphs are finite
Authors:
Martin Balko,
David Chodounský,
Jan Hubička,
Matěj Konečný,
Lluis Vena
Abstract:
We prove that the universal homogeneous 3-uniform hypergraph has finite big Ramsey degrees. This is the first case where big Ramsey degrees are known to be finite for structures in a non-binary language.
Our proof is based on the vector (or product) form of Milliken's Tree Theorem and demonstrates a general method to carry existing results on structures in binary relational languages to higher a…
▽ More
We prove that the universal homogeneous 3-uniform hypergraph has finite big Ramsey degrees. This is the first case where big Ramsey degrees are known to be finite for structures in a non-binary language.
Our proof is based on the vector (or product) form of Milliken's Tree Theorem and demonstrates a general method to carry existing results on structures in binary relational languages to higher arities.
△ Less
Submitted 3 July, 2021; v1 submitted 1 August, 2020;
originally announced August 2020.
-
Continuous and monotone machines
Authors:
Michal Konečný,
Florian Steinberg,
Holger Thies
Abstract:
We investigate a variant of the fuel-based approach to modeling diverging computation in type theories and use it to abstractly capture the essence of oracle Turing machines. The resulting objects we call continuous machines. We prove that it is possible to translate back and forth between such machines and names in the standard function encoding used in computable analysis. Put differently, among…
▽ More
We investigate a variant of the fuel-based approach to modeling diverging computation in type theories and use it to abstractly capture the essence of oracle Turing machines. The resulting objects we call continuous machines. We prove that it is possible to translate back and forth between such machines and names in the standard function encoding used in computable analysis. Put differently, among the operators on Baire space, exactly the partial continuous ones are implementable by continuous machines and the data that such a machine provides is a description of the operator as a sequentially realizable functional.
Continuous machines are naturally formulated in type theories and we have formalized our findings in Coq. Continuous machines, their equivalence to the standard encoding and correctness of basic operations are now part of Incone, a Coq library for computable analysis. While the correctness proofs use a classical meta-theory with countable choice, the translations and algorithms that are proven correct are all fully executable. Along the way we formally prove some known results such as existence of a self-modulating moduli of continuity for partial continuous operators on Baire space.
To illustrate their versatility we use continuous machines to specify some algorithms that operate on objects that cannot be fully described by finite means, such as real numbers and functions. We present particularly simple algorithms for finding the multiplicative inverse of a real number and for composition of partial continuous operators on Baire space. Some of the simplicity is achieved by utilizing the fact that continuous machines are compatible with multivalued semantics. We also connect continuous machines to the construction of precompletions and completions of represented spaces, topics that have recently caught the attention of the computable analysis community.
△ Less
Submitted 4 May, 2020;
originally announced May 2020.
-
Implementing evaluation strategies for continuous real functions
Authors:
Michal Konečný,
Eike Neumann
Abstract:
We give a technical overview of our exact-real implementation of various representations of the space of continuous unary real functions over the unit domain and a family of associated (partial) operations, including integration, range computation, as well as pointwise addition, multiplication, division, sine, cosine, square root and maximisation.
We use several representations close to the usua…
▽ More
We give a technical overview of our exact-real implementation of various representations of the space of continuous unary real functions over the unit domain and a family of associated (partial) operations, including integration, range computation, as well as pointwise addition, multiplication, division, sine, cosine, square root and maximisation.
We use several representations close to the usual theoretical model, based on an oracle that evaluates the function at a point or over an interval. We also include several representations based on an oracle that computes a converging sequence of rigorous (piecewise or one-piece) polynomial and rational approximations over the whole unit domain. Finally, we describe "local" representations that combine both approaches, i.e. oracle-like representations that return a rigorous symbolic approximation of the function over a requested interval sub-domain with a requested effort.
See also our paper "Representations and evaluation strategies for feasibly approximable functions" which compares the efficiency of these representations and algorithms and also formally describes and analyses one of the key algorithms, namely a polynomial-time division of functions in a piecewise-polynomial representation. We do not reproduce this division algorithm here.
△ Less
Submitted 10 October, 2019;
originally announced October 2019.
-
Big Ramsey degrees of 3-uniform hypergraphs
Authors:
Martin Balko,
David Chodounský,
Jan Hubička,
Matěj Konečný,
Lluis Vena
Abstract:
Given a countably infinite hypergraph $\mathcal R$ and a finite hypergraph $\mathcal A$, the big Ramsey degree of $\mathcal A$ in $\mathcal R$ is the least number $L$ such that, for every finite $k$ and every $k$-colouring of the embeddings of $\mathcal A$ to $\mathcal R$, there exists an embedding $f$ from $\mathcal R$ to $\mathcal R$ such that all the embeddings of $\mathcal A$ to the image…
▽ More
Given a countably infinite hypergraph $\mathcal R$ and a finite hypergraph $\mathcal A$, the big Ramsey degree of $\mathcal A$ in $\mathcal R$ is the least number $L$ such that, for every finite $k$ and every $k$-colouring of the embeddings of $\mathcal A$ to $\mathcal R$, there exists an embedding $f$ from $\mathcal R$ to $\mathcal R$ such that all the embeddings of $\mathcal A$ to the image $f(\mathcal R)$ have at most $L$ different colours.
We describe the big Ramsey degrees of the random countably infinite 3-uniform hypergraph, thereby solving a question of Sauer. We also give a new presentation of the results of Devlin and Sauer on, respectively, big Ramsey degrees of the order of the rationals and the countably infinite random graph. Our techniques generalise (in a natural way) to relational structures and give new examples of Ramsey structures (a concept recently introduced by Zucker with applications to topological dynamics).
△ Less
Submitted 10 June, 2019;
originally announced June 2019.
-
Extending partial automorphisms of $n$-partite tournaments
Authors:
Jan Hubička,
Colin Jahel,
Matěj Konečný,
Marcin Sabok
Abstract:
We prove that for every $n\geq 2$ the class of all finite $n$-partite tournaments (orientations of complete $n$-partite graphs) has the extension property for partial automorphisms, that is, for every finite $n$-partite tournament $G$ there is a finite $n$-partite tournament $H$ such that every isomorphism of induced subgraphs of $G$ extends to an automorphism of $H$. Our constructions are purely…
▽ More
We prove that for every $n\geq 2$ the class of all finite $n$-partite tournaments (orientations of complete $n$-partite graphs) has the extension property for partial automorphisms, that is, for every finite $n$-partite tournament $G$ there is a finite $n$-partite tournament $H$ such that every isomorphism of induced subgraphs of $G$ extends to an automorphism of $H$. Our constructions are purely combinatorial (whereas many earlier EPPA results use deep results from group theory) and extend to other classes such as the class of all finite semi-generic tournaments.
△ Less
Submitted 18 March, 2019;
originally announced March 2019.
-
All those EPPA classes (Strengthenings of the Herwig-Lascar theorem)
Authors:
Jan Hubička,
Matěj Konečný,
Jaroslav Nešetřil
Abstract:
In this paper we prove a general theorem showing the extension property for partial automorphisms (EPPA, also called the Hrushovski property) for classes of structures containing relations and unary functions, optionally equipped with a permutation group of the language. The proof is elementary, combinatorial and fully self-contained. Our result is a common strengthening of the Herwig-Lascar theor…
▽ More
In this paper we prove a general theorem showing the extension property for partial automorphisms (EPPA, also called the Hrushovski property) for classes of structures containing relations and unary functions, optionally equipped with a permutation group of the language. The proof is elementary, combinatorial and fully self-contained. Our result is a common strengthening of the Herwig-Lascar theorem on EPPA for relational classes with forbidden homomorphisms, the Hodkinson-Otto theorem on EPPA for relational free amalgamation classes, its strengthening for unary functions by Evans, Hubička and Nešetřil and their coherent variants by Siniora and Solecki. We also prove an EPPA analogue of the main results of J. Hubička and J. Nešetřil: All those Ramsey classes (Ramsey classes with closures and forbidden homomorphisms), thereby establishing a common framework for proving EPPA and the Ramsey property.
Our results have numerous applications, we include a solution of a problem related to a class constructed by the Hrushovski predimension construction.
△ Less
Submitted 23 January, 2022; v1 submitted 11 February, 2019;
originally announced February 2019.
-
Extending partial isometries of antipodal graphs
Authors:
Matěj Konečný
Abstract:
We prove EPPA (extension property for partial automorphisms) for all antipodal classes from Cherlin's list of metrically homogeneous graphs, thereby answering a question of Aranda et al. This paper should be seen as the first application of a new general method for proving EPPA which can bypass the lack of an automorphism-preserving completion. It is done by combining the recent strengthening of t…
▽ More
We prove EPPA (extension property for partial automorphisms) for all antipodal classes from Cherlin's list of metrically homogeneous graphs, thereby answering a question of Aranda et al. This paper should be seen as the first application of a new general method for proving EPPA which can bypass the lack of an automorphism-preserving completion. It is done by combining the recent strengthening of the Herwig--Lascar theorem by Hubička, Nešetřil and the author with the ideas of the proof of EPPA for two-graphs by Evans et al.
△ Less
Submitted 10 August, 2019; v1 submitted 14 January, 2019;
originally announced January 2019.
-
EPPA for two-graphs and antipodal metric spaces
Authors:
David Evans,
Jan Hubička,
Matěj Konečný,
Jaroslav Nešetřil
Abstract:
We prove that the class of finite two-graphs has the extension property for partial automorphisms (EPPA, or Hrushovski property), thereby answering a question of Macpherson. In other words, we show that the class of graphs has the extension property for switching automorphisms. We present a short, self-contained, purely combinatorial proof which also proves EPPA for the class of integer valued ant…
▽ More
We prove that the class of finite two-graphs has the extension property for partial automorphisms (EPPA, or Hrushovski property), thereby answering a question of Macpherson. In other words, we show that the class of graphs has the extension property for switching automorphisms. We present a short, self-contained, purely combinatorial proof which also proves EPPA for the class of integer valued antipodal metric spaces of diameter 3, answering a question of Aranda et al.
The class of two-graphs is an important new example which behaves differently from all the other known classes with EPPA: Two-graphs do not have the amalgamation property with automorphisms (APA), their Ramsey expansion has to add a graph, it is not known if they have coherent EPPA and even EPPA itself cannot be proved using the Herwig--Lascar theorem.
△ Less
Submitted 11 September, 2019; v1 submitted 28 December, 2018;
originally announced December 2018.
-
Forbidden cycles in metrically homogeneous graphs
Authors:
Jan Hubička,
Michael Kompatscher,
Matěj Konečný
Abstract:
In a recent paper by a superset of the authors it was proved that for every primitive 3-constrained space $Γ$ of finite diameter $δ$ from Cherlin's catalogue of metrically homogeneous graphs, there exists a finite family $\mathcal F$ of $\{1,\ldots, δ\}$-edge-labelled cycles such that a $\{1,\ldots, δ\}$-edge-labelled graph is a subgraph of $Γ$ if and only if it contains no homomorphic images of c…
▽ More
In a recent paper by a superset of the authors it was proved that for every primitive 3-constrained space $Γ$ of finite diameter $δ$ from Cherlin's catalogue of metrically homogeneous graphs, there exists a finite family $\mathcal F$ of $\{1,\ldots, δ\}$-edge-labelled cycles such that a $\{1,\ldots, δ\}$-edge-labelled graph is a subgraph of $Γ$ if and only if it contains no homomorphic images of cycles from $\mathcal F$. However, the cycles in the families $\mathcal F$ were not described explicitly as it was not necessary for the analysis of Ramsey expansions and the extension property for partial automorphisms.
This paper fills this gap by providing an explicit description of the cycles in the families $\mathcal F$, heavily using the previous result in the process. Additionally, we explore the potential applications of this result, such as interpreting the graphs as semigroup-valued metric spaces or homogenizations of $ω$-categorical $\{1,δ\}$-edge-labelled graphs.
△ Less
Submitted 22 March, 2023; v1 submitted 15 August, 2018;
originally announced August 2018.
-
A combinatorial proof of the extension property for partial isometries
Authors:
Jan Hubička,
Matěj Konečný,
Jaroslav Nešetřil
Abstract:
We present a short and self-contained proof of the extension property for partial isometries of the class of all finite metric spaces.
We present a short and self-contained proof of the extension property for partial isometries of the class of all finite metric spaces.
△ Less
Submitted 28 August, 2018; v1 submitted 28 July, 2018;
originally announced July 2018.
-
Combinatorial Properties of Metrically Homogeneous Graphs
Authors:
Matěj Konečný
Abstract:
Ramsey theory looks for regularities in large objects. Model theory studies algebraic structures as models of theories. The structural Ramsey theory combines these two fields and is concerned with Ramsey-type questions about certain model-theoretic structures. In 2005, Nešetřil initiated a systematic study of the so-called Ramsey classes of finite structures. This thesis is a contribution to the p…
▽ More
Ramsey theory looks for regularities in large objects. Model theory studies algebraic structures as models of theories. The structural Ramsey theory combines these two fields and is concerned with Ramsey-type questions about certain model-theoretic structures. In 2005, Nešetřil initiated a systematic study of the so-called Ramsey classes of finite structures. This thesis is a contribution to the programme; we find Ramsey expansions of the primitive 3-constrained classes from Cherlin's catalogue of metrically homogeneous graphs. A key ingradient is an explicit combinatorial algorithm to fill-in the missing distances in edge-labelled graphs to obtain structures from Cherlin's classes. This algorithm also implies the extension property for partial automorphisms (EPPA), another combinatorial property of classes of finite structures.
△ Less
Submitted 16 May, 2018;
originally announced May 2018.
-
On the Simultaneous Minimum Spanning Trees Problem
Authors:
Matěj Konečný,
Stanislav Kučera,
Jana Novotná,
Jakub Pekárek,
Martin Smolík,
Jakub Tětek,
Martin Töpfer
Abstract:
Simultaneous Embedding with Fixed Edges (SEFE) is a problem where given $k$ planar graphs we ask whether they can be simultaneously embedded so that the embedding of each graph is planar and common edges are drawn the same. Problems of SEFE type have inspired questions of Simultaneous Geometrical Representations and further derivations. Based on this motivation we investigate the generalization of…
▽ More
Simultaneous Embedding with Fixed Edges (SEFE) is a problem where given $k$ planar graphs we ask whether they can be simultaneously embedded so that the embedding of each graph is planar and common edges are drawn the same. Problems of SEFE type have inspired questions of Simultaneous Geometrical Representations and further derivations. Based on this motivation we investigate the generalization of the simultaneous paradigm on the classical combinatorial problem of minimum spanning trees. Given $k$ graphs with weighted edges, such that they have a common intersection, are there minimum spanning trees of the respective graphs such that they agree on the intersection? We show that the unweighted case is polynomial-time solvable while the weighted case is only polynomial-time solvable for $k=2$ and it is NP-complete for $k\geq 3$.
△ Less
Submitted 1 December, 2017;
originally announced December 2017.
-
Conant's generalised metric spaces are Ramsey
Authors:
Jan Hubička,
Matěj Konečný,
Jaroslav Nešetřil
Abstract:
We give Ramsey expansions of classes of generalised metric spaces where distances come from a linearly ordered commutative monoid. This complements results of Conant about the extension property for partial automorphisms and extends an earlier result of the first and the last author giving the Ramsey property of convexly ordered $S$-metric spaces. Unlike Conant's approach, our analysis does not re…
▽ More
We give Ramsey expansions of classes of generalised metric spaces where distances come from a linearly ordered commutative monoid. This complements results of Conant about the extension property for partial automorphisms and extends an earlier result of the first and the last author giving the Ramsey property of convexly ordered $S$-metric spaces. Unlike Conant's approach, our analysis does not require the monoid to be semi-archimedean.
△ Less
Submitted 17 September, 2019; v1 submitted 12 October, 2017;
originally announced October 2017.
-
Representations and evaluation strategies for feasibly approximable functions
Authors:
Michal Konečný,
Eike Neumann
Abstract:
A famous result due to Ko and Friedman (1982) asserts that the problems of integration and maximisation of a univariate real function are computationally hard in a well-defined sense. Yet, both functionals are routinely computed at great speed in practice. We aim to resolve this apparent paradox by studying classes of functions which can be feasibly integrated and maximised, together with represen…
▽ More
A famous result due to Ko and Friedman (1982) asserts that the problems of integration and maximisation of a univariate real function are computationally hard in a well-defined sense. Yet, both functionals are routinely computed at great speed in practice. We aim to resolve this apparent paradox by studying classes of functions which can be feasibly integrated and maximised, together with representations for these classes of functions which encode the information which is necessary to uniformly compute integral and maximum in polynomial time. The theoretical framework for this is the second-order complexity theory for operators in analysis which was introduced by Kawamura and Cook (2012). The representations we study are based on rigorous approximation by polynomials, piecewise polynomials, and rational functions. We compare these representations with respect to polytime reducibility as well as with respect to their ability to quickly evaluate symbolic expressions in a given language. We show that the representation based on rigorous approximation by piecewise polynomials is polytime equivalent to the representation based on rigorous approximation by rational functions. With this representation, all terms in a certain language, which is expressive enough to contain the maximum and integral of most functions of practical interest, can be evaluated in polynomial time. By contrast, both the representation based on polynomial approximation and the standard representation based on function evaluation, which implicitly underlies the Ko-Friedman result, require exponential time to evaluate certain terms in this language. We confirm our theoretical results by an implementation in Haskell, which provides some evidence that second-order polynomial time computability is similarly closely tied with practical feasibility as its first-order counterpart.
△ Less
Submitted 21 October, 2019; v1 submitted 10 October, 2017;
originally announced October 2017.
-
Minimal Sum Labeling of Graphs
Authors:
Matěj Konečný,
Stanislav Kučera,
Jana Novotná,
Jakub Pekárek,
Štěpán Šimsa,
Martin Töpfer
Abstract:
A graph $G$ is called a sum graph if there is a so-called sum labeling of $G$, i.e. an injective function $\ell: V(G) \rightarrow \mathbb{N}$ such that for every $u,v\in V(G)$ it holds that $uv\in E(G)$ if and only if there exists a vertex $w\in V(G)$ such that $\ell(u)+\ell(v) = \ell(w)$. We say that sum labeling $\ell$ is minimal if there is a vertex $u\in V(G)$ such that $\ell(u)=1$. In this pa…
▽ More
A graph $G$ is called a sum graph if there is a so-called sum labeling of $G$, i.e. an injective function $\ell: V(G) \rightarrow \mathbb{N}$ such that for every $u,v\in V(G)$ it holds that $uv\in E(G)$ if and only if there exists a vertex $w\in V(G)$ such that $\ell(u)+\ell(v) = \ell(w)$. We say that sum labeling $\ell$ is minimal if there is a vertex $u\in V(G)$ such that $\ell(u)=1$. In this paper, we show that if we relax the conditions (either allow non-injective labelings or consider graphs with loops) then there are sum graphs without a minimal labeling, which partially answers the question posed by Miller, Ryan and Smyth in 1998.
△ Less
Submitted 1 August, 2017;
originally announced August 2017.
-
Ramsey expansions of metrically homogeneous graphs
Authors:
Andrés Aranda,
David Bradley-Williams,
Jan Hubička,
Miltiadis Karamanlis,
Michael Kompatscher,
Matěj Konečný,
Micheal Pawliuk
Abstract:
We investigate Ramsey expansions, the coherent extension property for partial isometries (EPPA), and the existence of a stationary independence relation for all classes of metrically homogeneous graphs from Cherlin's catalogue. We show that, with the exception of tree-like graphs, all metric spaces in the catalogue have precompact Ramsey expansions (or lifts) with the expansion property. With two…
▽ More
We investigate Ramsey expansions, the coherent extension property for partial isometries (EPPA), and the existence of a stationary independence relation for all classes of metrically homogeneous graphs from Cherlin's catalogue. We show that, with the exception of tree-like graphs, all metric spaces in the catalogue have precompact Ramsey expansions (or lifts) with the expansion property. With two exceptions we can also characterise the existence of a stationary independence relation and coherent EPPA.
Our results are a contribution to Nešetřil's classification programme of Ramsey classes and can be seen as empirical evidence of the recent convergence in techniques employed to establish the Ramsey property, the expansion property, EPPA and the existence of a stationary independence relation. At the heart of our proof is a canonical way of completing edge-labelled graphs to metric spaces in Cherlin's classes. The existence of such a ``completion algorithm'' then allows us to apply several strong results in the areas that imply EPPA or the Ramsey property.
The main results have numerous consequences for the automorphism groups of the Fraisse limits of the classes. As corollaries, we prove amenability, unique ergodicity, existence of universal minimal flows, ample generics, small index property, 21-Bergman property and Serre's property (FA).
△ Less
Submitted 8 March, 2024; v1 submitted 9 July, 2017;
originally announced July 2017.
-
Completing graphs to metric spaces
Authors:
Andrés Aranda,
David Bradley-Williams,
Eng Keat Hng,
Jan Hubička,
Miltiadis Karamanlis,
Michael Kompatscher,
Matěj Konečný,
Micheal Pawliuk
Abstract:
We prove that certain classes of metrically homogeneous graphs omitting triangles of odd short perimeter as well as triangles of long perimeter have the extension property for partial automorphisms and we describe their Ramsey expansions.
We prove that certain classes of metrically homogeneous graphs omitting triangles of odd short perimeter as well as triangles of long perimeter have the extension property for partial automorphisms and we describe their Ramsey expansions.
△ Less
Submitted 4 March, 2019; v1 submitted 1 June, 2017;
originally announced June 2017.
-
Squarability of rectangle arrangements
Authors:
Matěj Konečný,
Stanislav Kučera,
Michal Opler,
Jakub Sosnovec,
Štěpán Šimsa,
Martin Töpfer
Abstract:
We study when an arrangement of axis-aligned rectangles can be transformed into an arrangement of axis-aligned squares in $\mathbb{R}^2$ while preserving its structure. We found a counterexample to the conjecture of J. Klawitter, M. Nöllenburg and T. Ueckerdt whether all arrangements without crossing and side-piercing can be squared. Our counterexample also works in a more general case when we onl…
▽ More
We study when an arrangement of axis-aligned rectangles can be transformed into an arrangement of axis-aligned squares in $\mathbb{R}^2$ while preserving its structure. We found a counterexample to the conjecture of J. Klawitter, M. Nöllenburg and T. Ueckerdt whether all arrangements without crossing and side-piercing can be squared. Our counterexample also works in a more general case when we only need to preserve the intersection graph and we forbid side-piercing between squares. We also show counterexamples for transforming box arrangements into combinatorially equivalent hypercube arrangements. Finally, we introduce a linear program deciding whether an arrangement of rectangles can be squared in a more restrictive version where the order of all sides is preserved.
△ Less
Submitted 22 November, 2016; v1 submitted 21 November, 2016;
originally announced November 2016.
-
Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
Authors:
Sewon Park,
Franz Brauße,
Pieter Collins,
SunYoung Kim,
Michal Konečný,
Gyesik Lee,
Norbert Müller,
Eike Neumann,
Norbert Preining,
Martin Ziegler
Abstract:
We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin po…
▽ More
We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin powerdomain and make our programming language semantics computable and complete: all and only real functions computable in computable analysis can be realized in ERC. The base programming language supports real arithmetic as well as implicit limits; expansions support additional primitive operations (such as a user-defined exponential function). By restricting integers to Presburger arithmetic and real coercion to the `precision' embedding $\mathbb{Z}\ni p\mapsto 2^p\in\mathbb{R}$, we arrive at a first-order theory which we prove to be decidable and model-complete. Based on said logic as specification language for preconditions and postconditions, we extend Hoare logic to a sound (w.r.t. the denotational semantics) and expressive system for deriving correct total correctness specifications. Various examples demonstrate the practicality and convenience of our language and the extended Hoare logic.
△ Less
Submitted 21 June, 2024; v1 submitted 20 August, 2016;
originally announced August 2016.
