A Simple Proof of Zorn’s Lemma

Just a personal rephrase of JONATHAN LEWIN’s simple proof of the Zorn Lemma, which I would really like to remember… so let’s work out all the details…

(… The proof is simple in the sense that it needs neither transfinite induction, nor Ordinals, just the Axiom of Choice (AC) and elementary extremality arguments …)

Theorem (Zorn’s Lemma). Suppose (X,\leq) is a partial order in which every chain is bounded from above. Then (X,\leq) has a maximal element.

Def. If C\subseteq X is a chain (i.e. total order) and x\in X, then \displaystyle I_C(x) = \{y\in C \mid y<x\} is named the initial segment of x in C.

Proof. Suppose (X,\leq) has no maximal element, towards a contradiction. If C is any chain in X, let u\in X be an upper bound of C. Since X has no maximal element, there exists v\in X such that u<v. So, C admits a strict upper bound. By AC, there is a choice function f which assigns to every chain C\subseteq X a strict upper bound f(C).

The sought contradiction will be that of finding a chain U\subseteq X such that f(U)\in U. This is catalysed by the following notion of conforming subset.

Def. Say that a subset A\subseteq X is conforming if the following two conditions hold:

  1. (A,\leq) is a well order (i.e. A is a chain such that every subset of A has a least element);
  2. for every a\in A, it holds a=f(I_A(a)).

Comparability Lemma. If A,B\subseteq X are conforming and A\neq B, then one of these two sets is an initial segment of the other.

Proof of Comparability Lemma. Since A\neq B we can assume w.l.o.g. A\setminus B\neq \emptyset.

Let x=\min (A\setminus B).

Then I_A(x)\subseteq B. So the Claim reduces to show B\subseteq I_A(x).

Towards a contradiction, assume B\setminus I_A(x) \neq \emptyset.

Let y = \min (B\setminus I_A(x)).

Let z = \min(A\setminus I_B(y)).

Closure Lemma. Given any u\in I_B(y), if v\in A and v<u then:

  • v<y (by definition of I_B(y) and y)
  • v\in B (since u\in I_B(y), so u\in I_A(x) by definition of y, thus v\in I_A(x) too, and I_A(x)\subseteq B by definition of x)

so v\in I_B(y).

With this, we can show that \displaystyle I_A(z)=I_B(y). Indeed, I_A(z)\subseteq I_B(y) follows already by definition of z, so the actual claim is that I_B(y)\subseteq I_A(z). Let u\in I_B(y), then u\in I_A(x) (by def. of y), so u\in A; also u\neq z (by def. of z); finally, it is not possible that u>z, otherwise by Closure Lemma it would be z\in I_B(y) against z own definition. Therefore, u<z. Since u\in A and u<z, then u\in I_A(z).

Also, z\leq x. Indeed, x\not\in B (by definition) so x\not\in I_B(y) but x\in A, therefore z\leq x (by definition of z at this point).

Since z=f(I_A(z))=f(I_B(y))=y, and since y\in B, we cannot have z=x (because x\not\in B by definition). Therefore, z<x, and we conclude y=z\in I_A(x), against definition of y.

This implies that B\setminus I_A(x) = \emptyset, i.e. B\subseteq I_A(x), closing the proof of the Comparability Lemma.

By the Comparability Lemma, it is clear that the union U of all conforming subsets of X is conforming. Thus, if x=f(U) is a strict upper bound, then U\cup \{x\} is conforming too. Since U is the union of all conforming sets, then x\in U , contradicting that x is a strict upper bound of U.

So (X,\leq) has one maximal element.

Instantaneous Reaction-Time in CSTNs on JLAMP

These days an extended version of our paper “Instantaneous Reaction-Time in Dynamic-Consistency Checking of Conditional Simple Temporal Networkshas been accepted for publication (to appear during March 2020, https://doi.org/10.1016/j.jlamp.2020.100542) in:

Journal of Logical and Algebraic Methods in Programming, Elsevier

0dcjlamp

Joint work with Massimo Cairo and Romeo Rizzi (Dept. of Computer Science, University of Verona, Italy)

Sorting with Forbidden Intermediates goes to DAM

An extended version of our paper “Sorting with Forbidden Intermediates (Searching (s,t)-Paths avoiding Forbidden Vertices in Hypercube Graphs)” has been accepted for publication in international journal (https://doi.org/10.1016/j.dam.2019.10.025):

Discrete Applied Mathematics, Elsevier

(journal of combinatorial algorithms, informatics and computational sciences).

Screenshot 2019-07-27 at 10.16.54.pngdownload

Joint work with Stéphane Vialette (CNRS and UPEM, Paris, France), Anthony Labarre (UPEM, Paris, France) and Romeo Rizzi (Univ. Verona, Italy).

Linear Time Alternating DFS and Safe-Alternating SCCs

An alternating graph is a directed graph whose vertex set is partitioned into two classes, existential and universal. This forms the basic arena for a plethora of infinite duration two-player games where Player \square and \circ alternate in a turn-based sliding of a pebble along the arcs they control.

We study alternating strongly-connectedness as a generalization of strongly-connectedness in directed graphs, aiming at providing a linear time decomposition and a sound structural graph characterization. For this a refined notion of alternating reachability is introduced: Player \square attempts to reach vertices without leaving a prescribed subset of the vertices, while Player \circ works against. This is named safe alternating reachability. It is shown that every arena uniquely decomposes into safe alternating strongly-connected components where Player \square can visit each vertex within a given component infinitely often, without having to ever leave out the component itself.

Our main result is a linear time algorithm for computing this alternating graph decomposition.

Both the underlying graph structures and the algorithm generalize the classical decomposition of a directed graph into strongly-connected components.
The algorithm builds on a linear time generalization of the depth-first search on alternation, taking inspiration from Tarjan 1972 machinery.

Our theory has direct applications in faster solving well-known infinite duration pebble games. Dinneen and Khoussainov showed in 1999 that deciding a given Update Game costs O(mn) time, where n is the number of vertices and m is that of arcs. We solve that task in \Theta(m+n) linear time. With this the complexity of Explicit McNaughton-Muller Games also improves from cubic to quadratic.

Download: manuscript, early draft presentation.

Screenshot 2019-06-09 at 13.15.47

Faster RDTPs at TIME2018

Our paper,

On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier,

has been accepted for publication at the 25th International Symposium on Temporal Representation and Reasoning (TIME 2018), to be held at Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland, 15-17 October 2018.

Joint work with Romeo Rizzi (Dept. of Computer Science, University of Verona, Italy).

Porting uavpal 4G/LTE drone soft_mod to the SkyController2P (Testing 4G/LTE for consumer UAVs communications)

Uavpal-disco4g and uavpal-beboptwo4g are software modifications for the Parrot Disco and Bebop2 french flag-3d-round-250 drones. Instead of the built-in regular wifi, the mod allows you to switch on a 4G/LTE cellular/mobile network connection to link the SkyController2 (SC2) to the flying drone 🙂 Control/telemetry and live video stream are routed through the 4G/LTE connection.

parrot-disco-flying

The soft mod is currently maintained by its original creator Marc B. (a.k.a. “softice”); it is a cheap, non-intrusive, rock solid and very enjoyable clever mod. It just works. However, the newest version of the Parrot SC2 — namely, the SkyController2P (SC2P) (the one having black plastic joysticks) — was not supported, not yet.buttons

I’ve succeeded at porting Marc’s original soft_mod to the SC2P. Here below you can find the corresponding complete shell script (if you have a SC2P, just replace or patch the original file uavpal_sc2.sh).

I wish to thank Marc for all of his great work, and for helpful discussions and advices which finally led me to code the following patch.

Experimental. Take off and fly at your own risk.

Download: uavpal_sc2.sh (script for the SkyController2P only, tested on sc2p-firmware v1.0.3 and v1.0.5)

bebop2

UPDATE (30/12/2018): SoftIce (uavpal’s maintainer) has finally merged my code supporting SC2P with the master-branch! Please find the patch below.
Ready take off
https://github.com/uavpal/disco4g/commit/b9e79dc8ab49f7cd433571773d092afc9c22151c

On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier.

In 2005 T.K.S. Kumar studied the Restricted Disjunctive Temporal Problem (RDTP), a restricted but very expressive class of Disjunctive Temporal Problems (DTPs). An RDTP comes with a finite set \mathcal{T}=\{X,Y,\ldots\} of time-point variables, and a finite set \mathcal{C} of temporal constraints where each of them can be either one of the following three types: (\texttt{t}_1) (Y-X\leq w), for w real (a simple temporal difference-constraint);
(\texttt{t}_2) (l_1\leq X\leq u_1)\vee \cdots \vee (l_k\leq X\leq u_k), for l_i,u_i reals (a single-variable disjunction of many interval-constraints);
(\texttt{t}_3) (l_1\leq X\leq u_1) \vee (l_2\leq Y\leq u_2), for l_i,u_i reals (a two-variable disjunction of two interval-constraints only).
Kumar showed that RDTPs are solvable in deterministic strongly-polynomial time by reducing them to the Connected Row-Convex (CRC) constraints problem; plus, he devised a randomized algorithm whose expected running time is less than that of the deterministic one. Instead, the most general form of DTPs allows for multi-variable disjunctions of many interval constraints and it is NP-complete.

This work offers a deeper comprehension on the tractability of RDTPs, leading to an elementary deterministic strongly-polynomial time algorithm for solving them,
significantly improving the asymptotic running times of all the previous deterministic and randomized algorithms. The result is obtained by reducing RDTPs to the Single-Source Shortest-Paths (SSSP) and the 2-SAT problem (jointly), instead of reducing to CRCs. In passing, we obtain a faster (quadratic time) algorithm for RDTPs having only \texttt{t}_1 and \texttt{t}_2-constraints (and no \texttt{t}_3-constraint).
As a second main contribution, we study the tractability frontier of solving RDTPs blended with Hyper Temporal Networks (HyTNs), a strict generalization of Simple Temporal Networks (STNs) grounded on hypergraphs: we prove that solving temporal problems having only \texttt{t}_2-constraints and either only multi-tail or only multi-head hyperarc-constraints lies in \text{NP}\cap \text{co-NP} and it admits deterministic pseudo-polynomial time algorithms; on the other hand, problems having only \texttt{t}_3-constraints and either only multi-tail or only multi-head hyperarc-constraints are strongly NP-complete.

Download: manuscript.

rdtps

A paper at TIME 2017

Our paper,

Incorporating Decision Nodes into Conditional Simple Temporal Networks

has been accepted at TIME 2017, to be held at Université de Mons, Belgium, Oct. 2017.

Abstract. A Conditional Simple Temporal Network (CSTN) is an extension of Simple Temporal Network (STN) having some special time-points, named observation time-points. In a STN/CSTN, the agent executing the network controls the execution of every time-point. Observation time-points have unique propositional letters associated with them and, when the agent executes one of them, the environment assigns a truth value to the corresponding propositional letter. Thus, the agent observes, but does not control, the assignment of truth values. A CSTN is dynamically consistent (DC) if there exists a strategy for executing its time-points such that all relevant constraints will be satisfied no matter which truth values the environment assigns to the propositional letters.

Alternatively, in a Labeled Simple Temporal Network (Labeled STN)—also called a Temporal Plan with Choice—the agent executing the network completely controls the process of assigning values to the so-called choice variables. Furthermore, the agent can make those assignments at any time.  For this reason, a Labeled STN is equivalent to a Disjunctive Temporal Network. A generalisation of the Bellman-Ford algorithm to accommodate the propagation of labeled values has been used to determine whether any given Labeled STN is consistent.

This paper incorporates both of the above extensions by augmenting a CSTN to include not only observation time-points, but also decision time-points. A decision time-point is like an observation time-point in that it has an associated propositional letter whose value is determined when the decision time-point is executed.  It differs in that the agent (not the environment) selects that value.  The resulting network is called a CSTN with Decisions (CSTND). This paper shows that a CSTND generalizes both CSTNs and Labeled STNs. It proves that the decision problem of determining whether or not any CSTND is dynamically consistent is PSPACE-complete. And it  presents algorithms that restrict attention to two special classes of CSTNDs: (i) those that contain only decision time-points; and (ii) those in which all decisions are made before starting to execute the network.

Download: paper.