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
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02102002
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:11:45 AM
Last modification on : Sunday, April 28, 2019 - 1:23:01 AM

File

RR2007-14.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02102002, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

3

Files downloads

9