Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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

Abstract : 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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Colette ORANGE Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:11:45 AM
Last modification on : Wednesday, October 26, 2022 - 8:14:12 AM


Files produced by the author(s)


  • HAL Id : hal-02102002, version 1



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⟩



Record views


Files downloads