Acyclicity and Finite Linear Extendability: a Formal and Constructive Equivalence. - LARA - Libre accès aux rapports scientifiques et techniques
Rapport (Rapport De Recherche) Année : 2007

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

Résumé

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.
Fichier principal
Vignette du fichier
RR2007-14.pdf (244.75 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02102002 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02102002 , version 1

Citer

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⟩
37 Consultations
89 Téléchargements

Partager

More