Acyclicity and Finite Linear Extendability: a Formal and Constructive Equivalence.

Stéphane Le Roux (1)

1 LIP - Laboratoire de l'Informatique du Parallélisme

Linear extension of partial orders emerged in the late 1920's. Its computer-oriented version, \emph{i.e.}, topological sorting of finite partial orders, arose in the late 1950's. However, those issues have not yet been considered from a viewpoint that is both formal and constructive; this paper discusses a few related claims formally proved with the constructive proof assistant Coq. For instance, it states that a given decidable binary relation is acyclic and equality is decidable on its domain \emph{iff} an irreflexive linear extension can be computed uniformly for any of its finite restriction. A detailed introduction and proofs written in plain English shall help readers who are not familiar with constructive issues or Coq formalism.

Mots clés: Induction; Topological sorting; (non-)uniform computability; Binary relation; Constructivism; Finite restriction; Linear extension; Proof assistant

Mots clés: Relation binaire; restriction finie; extension linéaire; calculabilité (non-)uniforme; tri topologique; constructisme; récurrence; assistant à la preuve

Domaines: Informatique [cs]

Stéphane Le Roux. Acyclicity and Finite Linear Extendability: a Formal and Constructive Equivalence.. [Research Report] LIP RR-2007-14, Laboratoire de l'informatique du parallélisme. 2007, 2+22p. ⟨hal-02102002⟩