PhD Guillaume Thébault
email: guillaume.thebault@univ-st-etienne.fr

MSc Arthur-Henri Michalland
email: arthur-henri.michalland@univ-montp3.fr

PhD Vincent Dérozier
email: vincent.derozier@mines-ales.fr

MD Stéphane Chabrier
email: stephane.chabrier@univ-st-etienne.fr

PhD Denis Brouillet
email: denis.brouillet@univ-montp3.fr

When the vibrations allow for anticipating the force to be produced: an extend to Pfister et al. (2014)

Keywords: Action, anticipation, tactile effects, body, ideomotor theory

According to the Ideomotor Theory, action selection is done by the mental anticipation of its perceptual consequences. If the distal information processed mainly by vision and hearing are considered essential for the representation of the action, the proximal information processed by the sense of touch and proprioception is of less importance. Recent works seem to show the opposite. Nevertheless, it is necessary to complete these results by offering a situation, more ecological, where response and effect can occur on the same effector. So, the goal of our work was to implement a more relevant spatial correspondence because to touch is not the same action that to hear or to see.

To do so, participants pressed a specific key after the presentation of a stimulus. The key vibrated depending on the pressure exerted on it. In a compatible condition, high pressure on a key triggered a high vibration, while in an incompatible condition high pressure triggered a low vibration on the same effectors. As expected, the response times were faster in the compatible condition than the incompatible condition. This means that proximal information participates actively in the selection of action.

Introduction

Every action we perform causes specific effects in the environment. For instance, pressing a doorbell triggers a ring and consequences for inhabitant behaviour: opening the door. If you know that a baby sleeps in this home, you will delicately press the doorbell with your hand hoping that it will not wake up the baby. Schematically, a stimulus (the doorbell) is associated with a perceptual effect (bell ringing) and a response (to press). Similarly, ideomotor theory postulates that an idea, or an image, based on perceptual and body effects of actions, is enough to activate action representations [START_REF] James | The principles of psychology[END_REF][START_REF] Lotze | Medicinische Psychologie oder Physiologie der Seele [Medical psychology or the physiology of the mind[END_REF].

The modern conception of the ideomotor theory propose that actions are selected by their "auditory, visual, proprioceptive, kinesthetic and/or tactile" (Grenwald 1970, p.51) consequences. However, the theoretical issue of what effects are coded in action is still open [START_REF] Shin | A review of contemporary ideomotor theory[END_REF].

Specifically, tactile or proprioceptive effects are presupposed to be more marginal than auditory and visual effects [START_REF] Osiurak | Pliers, not fingers: Tool-action effect in a motor intention paradigm[END_REF][START_REF] Pfister | Dissecting the response in response-effect compatibility[END_REF]. For instance, in the Theory of Event Coding (TEC, [START_REF] Hommel | The theory of event coding (TEC): A framework for perception and action planning[END_REF] there is a distinction between the distal events related to objects of environment and proximal events than concern the physical perception like body sensations. By drawing on the need to constantly refer on our kinaesthetic and tactile perceptions, the Theory "assumes that action planning is based on distal representations" (Hommel, 2009, p. 516). This position is also the one of James (1890).

Derived from the Greenwald paradigm, Hommel and collaborators (Elsner andHommel 2001, 2004;[START_REF] Hommel | The theory of event coding (TEC): A framework for perception and action planning[END_REF] proposed a two-phase procedure to explore distal effects. In the first phase, participants pressed right or left keys after the presentation of a white rectangle. Each response key triggered a tone; for instance, the right key triggered a high tone, while the left key triggered a low tone. In the test phase, the tone was presented and participants pressed the key as quickly as possible. In one condition, the relations between tone and response key were similar to the acquisition phase; in another condition, the tone and response key were different. [START_REF] Elsner | Effect anticipation and action control[END_REF] showed that participants were faster to press the key in the similar condition than the non-similar condition. Recently, it has been showed that proprioceptive perceptions were integrated in the same representation as action [START_REF] Camus | Assessing the functional role of motor response during the integration process[END_REF][START_REF] Camus | From anticipation to integration: the role of integrated action-effects in building sensorimotor contingencies[END_REF]. So, the proximal effects could be less marginal than what is mentioned in TEC.

These proximal effects were more specifically explored with the response-effect compatibility paradigm [START_REF] Kunde | Response-effect compatibility in manual choice reaction tasks[END_REF]. Indeed, for [START_REF] Kunde | Response-effect compatibility in manual choice reaction tasks[END_REF], the anticipation of action cannot be demonstrated if the effect precedes the participant's response as used in [START_REF] Elsner | Effect anticipation and action control[END_REF] experiments. Thus, he proposed a procedure that does not require a test phase, and where effects always occur after responses. This procedure is simple and relatively similar to our example and other ecological learning situations. For instance, pressing a key triggers a tone. In one condition (compatible condition), the pressure exerted on the key is compatible with the intensity of the tone (i.e., high pressure triggers a high tone), while in the second condition (incompatible condition) the pressure exerted will be followed by an incompatible tone (i.e., low pressure triggers a high tone). [START_REF] Kunde | Response-effect compatibility in manual choice reaction tasks[END_REF] found that response times were faster in the compatible condition than in the incompatible condition, showing the role of distal effects in the anticipation of action.

Recently, based on Kunde's paradigm, [START_REF] Pfister | Good vibrations? Vibrotactile self-stimulation reveals anticipation of body-related action effects in motor control[END_REF] and [START_REF] Wirth | Stroking me softly: Body-related effects in effect-based action control[END_REF] specifically explored proximal effects (see also ten [START_REF] Hoopen | Vibrotactual choice reaction time, tactile receptor systems and ideomotor compatibility[END_REF]. They used a response-effect compatibility paradigm where participants answer to a stimulus and responses were followed by a tactile effect. For instance, in the first experiment of [START_REF] Pfister | Good vibrations? Vibrotactile self-stimulation reveals anticipation of body-related action effects in motor control[END_REF], after a stimulus presentation, participants pressed a response key which vibrated according to a spatial condition (i.e., compatible condition, the key pressed vibrates) or according to an incompatible spatial condition (i.e., the opposite key vibrates). The results showing faster answers in the compatible than incompatible were only found in the fifth quintile, but indicated an anticipation of actions depending on body effects. [START_REF] Pfister | Good vibrations? Vibrotactile self-stimulation reveals anticipation of body-related action effects in motor control[END_REF] interpreted these small effects as being due to the methodology used. In fact, in ecological situations if actions performed by the right hand can trigger auditory or visual effects on the left, there are few activities where the right hand triggers a body effect in the left hand. For [START_REF] Wirth | Stroking me softly: Body-related effects in effect-based action control[END_REF], the small effect found by [START_REF] Pfister | Good vibrations? Vibrotactile self-stimulation reveals anticipation of body-related action effects in motor control[END_REF] could also be task-relevant so they proposed a new task. After the presentation of a stimulus (Stimulus), the participants moved a slider with one hand (Response) connected to a brush stimulating the opposite forearm (Effect). In one condition, the movement of the hand was similar to the movement of the brush on the skin of the opposite forearm (compatible condition), while in another condition, these movements were incompatible. Results showed a main effect of compatibility with response times being faster in the compatible condition than incompatible condition. These two studies appear to provide evidence in favour of tactile effects in the anticipation of an action.

Nevertheless, if for distal information spatial correspondence between movement of hand and effects is probably always integrated during action, for proximal information it seems necessary to compare conditions which are which similar in ecological situations. Thus, it is quite unlikely in daily life to touch an object with left hand and to perceive consecutively a tactile effect with right hand (case of the study of [START_REF] Pfister | Good vibrations? Vibrotactile self-stimulation reveals anticipation of body-related action effects in motor control[END_REF]. What is possible with auditory or visual effects is not appropriate with tactile effects.

To extend previous works on anticipation of action by tactile effects, we believe that it is crucial to match response, spatial compatibility and effect in the context of touch because an artificial compatibility could affect response times. In other words, we believe that response and effect must concern the same effector, that is to say the finger doing the action. . Building on Pfister et al.'s (2014) and [START_REF] Kunde | Response-effect compatibility in manual choice reaction tasks[END_REF] studies, we proposed an experiment without spatial compatibility between response and effect to be more similar to an ecological situation. Our introductory example is a typical situation where pressing a key needs tactile afferences of the same hand. Indeed, despite your best endeavours, if you feel your finger sinking into the doorbell, you will expect to hear the baby crying. In our study, we designed a procedure to measure in the same location the effects of compatibility of pressure and vibration effects. We expected faster answers when high pressure was associated with a high vibration effect or low pressure was associated with a low vibration effect (i.e., compatible condition) in comparison to answers where high pressure was associated with a low vibration effect or low pressure was associated with a high vibration (i.e., incompatible condition).

Methods

Participants

Thirty-two participants took part in the experiment. All were naïve about the experiment's purpose and gave their free consent after being informed about study. The number of participants was in accordance with results carried out by GPower software [START_REF] Faul | G* Power 3: A flexible statistical power analysis program for the social, behavioral, and biomedical sciences[END_REF]).

Materials

We created two specific response keys for our experiment (Fig1a). On one side of the key, we placed a Force Sensitive Resistor (FSR, FSR-402 from Interlink Electronics, Santa Barbara, CA, USA, cf. Fig1a on the right) with a round sensing area 0.5" in diameter. On the other side, we put a vibration motor like those used in a Smartphone (cf. Fig1a on the left). These keys were controlled by an Arduino interface (Arduino Leonardo, Somerville, MA, USA) that creates keyboard responses from captors (Fig1b). We calculated two distinct forces of pressure needed to trigger a response. The force to trigger low pressure was up to 25cN while the force needed to trigger high pressure was up to 77cN. The vibrations oscillated in two different frequencies determined by the Arduino programme resulting in high or low vibrations. The frequencies of high vibrations were twice as high as low vibrations.

Concretely, the key response vibrated according to two different levels as a function of the force of pressure exerted on the FSR by participants.

Stimuli and procedure

The experiment was conducted in an isolated room. The participants seated in front of a computer with forearms on the table. Hands were placed at a similar distance from the middle of the screen. We instructed them to grasp a specific key (cf. Fig1a) between their thumb and their finger, as if they were grasping a key or a coin. The stimuli, two capital letters (H and X, Droid sans mono, 60pt), were presented for 250ms in the centre of a 17" screen. The letters were in white on a black background.

Participants were asked to press the response keys according to two levels of pressure depending on the stimuli (e.g., right key for H and left key for X). The participants had to exert strong pressure on one key and low pressure on the other key as quickly as possible when the letters appeared. The vibrations (low vs high) were triggered after a 200ms delay once the level of pressure had been reached. The duration of the vibration was 250ms.

Participants had 1500ms to respond after the presentation of stimuli. Then, the next trial started after an interval of 1000ms. Participants completed ten blocks of 16 trials in the compatible and incompatible conditions. The order of presentation of experimental conditions was counterbalanced. Half of the participants used their right hand to exert high pressure.

Results

Errors produced by participants (6.25%) and responses under 150ms and exceeding 1250ms were removed from the statistical analysis. Then, for each participant, we applied a filter to exclude the responses at 2.5 SD above and below the mean in each condition of compatibility. We calculated quintiles of distributions for each participant and condition.

To examine the response times by quintiles in each condition, a 2 x 5 analysis of variance (ANOVA) was carried out to test the principal effects of compatibility and quintile, and then interaction effects. We found a significant effect of compatibility (F(1, 31) = 4.74, p = .04, η² p =.13); participants responded faster in the compatible condition than in the incompatible and a significant effect of quintile was found as expected (F(31, 124)= 386, p < .001, η² p = .96). As shown in Fig2, a significant interaction effect was found (F(4, 24) = 6.41, p < .0001).

Analysis of this interaction showed only a significant effect for the higher quintile (p = .01, η² p = .51).

Fig 2 Results by quintiles of compatible and incompatible conditions

Discussion

The aim of this study was to provide evidence for the role of tactile effects in the anticipation of actions while the ideomotor theory implies that the proximal information processed by proprioception is of less importance for the representation of actions [START_REF] Osiurak | Pliers, not fingers: Tool-action effect in a motor intention paradigm[END_REF][START_REF] Pfister | Dissecting the response in response-effect compatibility[END_REF]. If it is well established that distal effects (i.e., visual or auditory) are important for anticipation of action (e.g., [START_REF] Elsner | Effect anticipation and action control[END_REF][START_REF] Kunde | Response-effect compatibility in manual choice reaction tasks[END_REF][START_REF] Kunde | Anticipated action effects affect the selection, initiation, and execution of actions[END_REF]), few studies have shown a similar role for proximal effects [START_REF] Pfister | Good vibrations? Vibrotactile self-stimulation reveals anticipation of body-related action effects in motor control[END_REF][START_REF] Wirth | Stroking me softly: Body-related effects in effect-based action control[END_REF].

Unlike [START_REF] Pfister | Good vibrations? Vibrotactile self-stimulation reveals anticipation of body-related action effects in motor control[END_REF], in our study, response and effect concerned the same effector (i.e. the finger doing the action). Our results highlighted that response times were faster when strongly (or weakly) pressing the response key was followed by a strong (or weak) tactile vibration than when response and effects were presented in an incompatible condition. Furthermore, we also observed an interaction effect of compatibility and quintile.

More precisely like [START_REF] Kunde | Response-effect compatibility in manual choice reaction tasks[END_REF], [START_REF] Pfister | Good vibrations? Vibrotactile self-stimulation reveals anticipation of body-related action effects in motor control[END_REF] and [START_REF] Wirth | Stroking me softly: Body-related effects in effect-based action control[END_REF], a significant effect of compatibility was found only in the last quintile of the distribution. So, as expected, tactile effects are well anticipated before response initiation.

If Pfister et al.'s (2014) results could be interpreted by the spatial coding brought about by tactile effects occurring during a task, our results were supported by tactile effects features. Thus, we strengthen the hypothesis that tactile effects play the same role as distal effects, highlighting the role of proximal effects in the ideomotor mechanism [START_REF] James | The principles of psychology[END_REF][START_REF] Badets | A review of ideomotor approaches to perception, cognition, action, and language: Advancing a cultural recycling hypothesis[END_REF][START_REF] Pfister | Good vibrations? Vibrotactile self-stimulation reveals anticipation of body-related action effects in motor control[END_REF][START_REF] Wirth | Stroking me softly: Body-related effects in effect-based action control[END_REF].

Another explanation could take into account the origin of tactile stimulation. Indeed, we may wonder whether all the tactile vibrations really activate proximal effects whereas body sensations are either environment-related or related the activity of the agent1 . Thus, an assumption to be considered is that tactile effects following an action are distinguished by the subject as two distinct events by the source of sensation (Djikerman and De Haan 2007).

Tactile proximal effects would be the sensations perceived by the subject when acting; tactile distal effects would be the sensations perceived by the subject when triggered by an event in the environment. This argument is legitimate insofar as our results are very similar to others [START_REF] Kunde | Response-effect compatibility in manual choice reaction tasks[END_REF][START_REF] Pfister | Good vibrations? Vibrotactile self-stimulation reveals anticipation of body-related action effects in motor control[END_REF][START_REF] Wirth | Stroking me softly: Body-related effects in effect-based action control[END_REF] highlighting the involvement of external stimuli (i.e., distal effects) and not those "internal to the body" (i.e., proximal effects). For instance, blind subject can perceive objects in the environment with sensory stimulations delivered via a specific device, but only if the subject is in an active exploration involving moto-sensory processes [START_REF] Bach-Y-Rita | Vision substitution by tactile projection[END_REF][START_REF] Gapenne | The co-constitution of the self and the world: Action and proprioceptive coupling[END_REF]; see also [START_REF] Varela | The embodied mind: Cognitive science and human experience[END_REF]. Interestingly, the perception of tactile sensors from a device is sometimes abolished by sensation arising from the environment, generating confusion between internal and external bodily events [START_REF] Auvray | There is something out there: distal attribution in sensory substitution, twenty years later[END_REF][START_REF] Gapenne | The co-constitution of the self and the world: Action and proprioceptive coupling[END_REF]).

This argument leads us to think that proximal -distal might not be relevant. Indeed, a tactile stimulus is both distal (i.e., its origin via proprioceptive sensations) and proximal (i.e., the sensation it triggers).

So, we could consider the role of touch like another proximal effect grouping sensations and movements since movement is at the core of ideomotor mechanisms [START_REF] James | The principles of psychology[END_REF]. Previous research found a correspondence between force exerted with digits and perceptive effects allowing one to select and to initiate movement on the principle of bidirectional relations between motor and perceptual codes [START_REF] Kunde | Response-effect compatibility in manual choice reaction tasks[END_REF][START_REF] Kunde | Anticipated action effects affect the selection, initiation, and execution of actions[END_REF]).

These relations reflect the integrative process during action [START_REF] Blanchard | Differential contributions of vision, and muscle proprioception to the coding of hand movements[END_REF][START_REF] Camus | Assessing the functional role of motor response during the integration process[END_REF][START_REF] Camus | From anticipation to integration: the role of integrated action-effects in building sensorimotor contingencies[END_REF]. Taken together, anticipation of tactile and proprioceptive effects produced by movement, which encompasses motor control via the musculoskeletal framework [START_REF] Kavounoudias | Proprio-tactile integration for kinesthetic perception: An fMRI study[END_REF][START_REF] Stillman | Making sense of proprioception: The meaning of proprioception, kinaesthesia and related terms[END_REF], still need to be explored.

Fig 1

 1 Fig 1 The keys were composed on one face by a motor and on other face by a force sensitive response (Fig1a, on the left). These keys were controlled by an Arduino interface (Fig1b, on the right)

Remote versus resident effects for[START_REF] Shin | A review of contemporary ideomotor theory[END_REF].

Funding

This research did not receive any specific grant from funding agencies in the public, commercial, or not-for-profit sectors.


Stéphane Le

Roux Mar

Acyclicity and Finite Linear Extendability: a Formal and Constructive Equivalence

Keywords: Binary relation, finite restriction, linear extension, (non-)uniform computability, topological sorting, constructivism, induction, proof assistant Relation binaire, restriction finie, extension linéaire, calculabilité (non-)uniforme, tri topologique, constructisme, récurrence

Linear extension of partial orders emerged in the late 1920's. Its computer-oriented version, 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 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.

Introduction

This section adopts an approach technical and historical. It presents three issues: the main ingredients of the proof assistant Coq, namely inductive methods, constructivism, the Curry-De Bruijn-Howard correspondence, and constructive proof assistant in general; the notions of computability and linear extension, both involved in the results proved in Coq and discussed in this paper; the main results and the contents of the paper.

A Historical View on Inductive Methods

Acerbi [START_REF] Acerbi | Plato: Parmenides 149a7-c3. a proof by complete induction?[END_REF] identifies the following three stages in the history of proof by induction. First, an early intuition can be found in Plato's Parmenides. Second, in 1575, Maurolico [START_REF] Maurolico | Arithmeticorum libri duo[END_REF] showed by an inductive argument that the sum of the first n odd natural numbers equals n 2 . Third, Pascal seems to have performed fully conscious inductive proofs. Historically, definitions by induction came long after proofs by induction. In 1889, even though the Peano's axiomatization of the natural numbers [START_REF] Peano | Arithmetices principia, nova methodo exposita[END_REF] referred to the successor of a natural, it was not yet an inductive definitionbut merely a property that had to hold on pre-existing naturals. Early XXth century, axiomatic set theory enabled inductive definitions of the naturals, like von Neumann [START_REF] John Von Neumann | Zur Einfürung der transfiniten Zahlen[END_REF], starting from the empty set representing zero. Beside the natural numbers, other objects also can be inductively/recursively defined. According to Gochet and Gribomont [START_REF] Gochet | Logique, méthode pour l'informatique fondamentale[END_REF], primitive recursive functions were introduced by Dedekind and general recursive functions followed works of Herbrand and Gödel; since then, it has been also possible to define sets by induction, as subsets of known supersets. However, the inductive definition of objects from scratch, i.e., not as part of a greater collection, was mainly developed through recursive types (e.g., lists or trees).

Constructivism in Proof Theory

Traditional mathematical reasoning is ruled by classical logic. First attempts to formalize this logic can be traced back to ancient Greeks like Aristotle [START_REF] Organon | Prior Analytics[END_REF] who discussed the principle of proof by contradiction among others: to prove a proposition by contradiction, one first derives an absurdity from the denial of the proposition, which means that the proposition can not not hold. From this, one eventually concludes that the proposition must hold. This principle is correct with respect to classical logic and it yields elegant and economical proof arguments. For example, a proof by contradiction may show the existence of objects complying with a given predicate without exhibiting a constructed witness: if such an object can not not exist then it must exist. At the beginning of the XXth century, many mathematicians started to think that providing an actual witness was a stronger proof argument. Some of them, like Brouwer, would even consider the proof by contradiction as a wrong principle. This mindset led to intuitionistic logic and, more generally, to constructivist logics formalized by Heyting, Gentzen, and Kleene among others. Instead of the principle of proof by contradiction, intuitionists use a stricter version stating only that an absurdity implies anything. Intuitionistic logic is smaller than classical logic in the sense that any intuitionistic theorem is also a classical theorem, but the converse does not hold. In [START_REF] Troelstra | Constructivism in mathematics. An introduction[END_REF], a counter-example shows that the intermediate value theorem is only classical, which implies the same for the Brouwer fixed point theorem. The principle of excluded middle states that any proposition is either "true" or "false". It is also controversial and it is actually equivalent, with respect to intuitionistic logic, to the principle of proof by contradiction. Adding any of those two principles to the intuitionistic logic yields the classical logic. In this sense, each of those principles captures the difference between the two logics.

The Curry-De Bruijn-Howard Correspondence

Nowadays, intuitionistic logic is also of interest due to practical reasons: the Curry-De Bruijn-Howard correspondence identifies intuitionistic proofs with functional computer programs and propositions with types. For example a program f of type A → B is an object requiring an input of type A and returning an output of type B. By inhabiting the type A → B, the function f is also a proof of "A implies B ". This vision results from many breakthroughs in proof and type theories: type theory was first developed by Russell and Whitehead in [START_REF] North | Principia Mathematica[END_REF] in order to cope with paradoxes in naive set theory. People like Brouwer, Heyting, and Kolmogorov had the intuition that a proof was a method (or an algorithm, or a function), but could not formally state it at that time. In 1958, Curry saw a connection between his combinators and Hilbert's axioms. Later, Howard [START_REF] Seldin | Essays on Combinatory Logic, Lambda Calculus and Formalism[END_REF] made a connection between proofs and lambda terms. Eventually, De Bruijn [START_REF]Selected Papers on Automath[END_REF] stated that the type of a proof was the proven proposition.

Constructive Proof Assistants

The Curry-De Bruijn-Howard Correspondence led to rather powerful proof assistants. Those pieces of software verify a proof by checking whether the program encoding the proof is well-typed. Accordingly, proving a given proposition amounts to providing a program of a given type. Some basic proof-writing steps are automated but users have to code the "interesting" parts of the proofs themselves. Each single step is verified, which gives an additional guarantee of the correctness of a mathematical proof. Of course this guarantee is not absolute: technology problems (such as software or hardware bugs) may yield validation of a wrong proof and human interpretations may also distort a formal result. Beside level of guarantee, another advantage is that a well-structured formal proof can be translated into natural language by mentioning all and only the key points from which a full formal proof can be easily retrieved. Such a reliable summary is usually different from the sketch of a "proof" that has not been actually written. An advantage of intuitionistic logic over classical logic is that intuitionistic proofs of existence correspond to search algorithms and some proof assistants, like Coq, are able to automatically extract an effective search program from an encoded proof, and the program is certified for free. See the Coq website [START_REF]The Coq proof assistant[END_REF] and the book by Bertot and Casteran [START_REF] Berthot | Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions[END_REF].

Decidability and Computability

In the middle of the 1930's, Church introduced the lambda calculus, and Turing and Post independently designed their very similar machines. Those three notions are by some means equivalent models for computer programs. A question is said to be decidable if there exists a computer program (equivalently lambda term or Post-Turing machine) requiring the parameters of the questions as input, returning (within finite time) "yes" or "no" as output, and thus correctly answering the question. In this way, a binary relation over a set is said to be decidable if there exists a program expecting two elements in that set and returning "yes" if they are related or "no" if they are not. A sister notion is that of computable (or recursive) function, i.e., mathematical function the images of which are computable within finite time by the same computer program although the domain and the codomain of the function may be infinite. Note that computability with two-element-codomain functions amounts to decidability. If several computable functions can be all computed by the same program, then these functions are said to be uniformly computable.

Transitive Closure, Linear Extension, and Topological Sorting

The calculus of binary relations was developed by De Morgan around 1860. The notion of transitive closure of a binary relation (smallest transitive binary relation including a given binary relation) was defined in different manners by different people about 1890. See Pratt [START_REF] Pratt | Origins of the calculus of binary relations[END_REF] for a historical account. In 1930, Szpilrajn [START_REF] Szpilrajn | Sur l'extension de l'ordre partiel[END_REF] proved that, assuming the axiom of choice, any partial order has a linear extension, i.e., is included in some total order. The proof invokes a notion close to transitive closure. Szpilrajn acknowledged that Banach, Kuratowsky, and Tarski had found unpublished proofs of the same result. In the late 1950's, The US Navy [3] designed PERT (Program Evaluation Research Task or Project Evaluation Review Techniques) for management and scheduling purposes. This tool partly consists in splitting a big project into small jobs on a chart and expressing with arrows when one job has to be done before another one can start up. In order to study the resulting directed graph, Jarnagin [START_REF] Jarnagin | Automatic machine methods of testing pert networks for consistency[END_REF] introduced a finite and algorithmic version of Szpilrajn's result. This gave birth to the widely studied topological sorting issue, which spread to the industry in the early 1960's (see [START_REF] Daniel | Topological ordering of a list of randomly-numbered elements of a network[END_REF] and [START_REF] Kahn | Topological sorting of large networks[END_REF]). Some technical details and computer-oriented examples can be found in Knuth's book [START_REF] Knuth | The Art of Computer Programming[END_REF].

Contribution

This paper revisits a few folklore results involving transitive closure, excluded middle, computability, linear extension, and topological sorting. Most of the properties are logical equivalences instead of one-way implications, which suggests maximal generality. Claims have been fully formalized (and proved) in Coq and then slightly modified in order to fit in the Coq-related CoLoR library [START_REF] Blanqui | CoLoR, a Coq Library on rewriting and termination[END_REF]. This paper follows the structure of the underlying Coq development but some straightforward results are omitted. Arguments are constructive (therefore also classical) and usually simple. This paper is meant to be read by a mathematician who is not familiar with constructivism. Concepts specific to Coq are introduced before they are used. Formal definitions and results are stated in a light Coq formalism that is very close to traditional mathematics and slightly different from the actual Coq code in order to ease the reading. Proofs are mostly written in plain English. The main result in this paper relies on an intermediate one, and is itself invoked in a game theoretic proof (in Coq) not published yet.

In this paper, a binary relation over an arbitrary set is said to be middle-excluding if for any two elements in the set, either they are related or they are not. The intermediate result of this paper implies that in an arbitrary set with decidable (resp. middle-excluding) equality, a binary relation is decidable (resp. middle-excluding) iff the transitive closures of its finite restrictions are uniformly decidable (resp. middle-excluding). The main result splits into two parts, one on excluded middle and one on computability: First, consider a middle-excluding relation. It is acyclic and equality on its domain is middle-excluding iff its restriction to any finite set has a middle-excluding irreflexive linear extension. Second, consider R a decidable binary relation over A. The following three propositions are equivalent.

a Formal and Constructive Equivalence

Note that computability of linear extensions is non-uniform in the second proposition but uniform in the third one.

• Equality on A is decidable and R is acyclic.

• Equality on A is decidable and every finite restriction of R has a decidable linear extension.

• There exists a computable function that expects finite restrictions of R and returns (decidable) linear extensions of them.

Contents

Section 2 gives a quick look at the Coq versions of types, binary relations, excluded middle, and computability. Through the example of lists, section 3 explains the principle of definition by induction in Coq, as well as the associated inductive proof principle and definition by recursion. In particular, subsection 3.2 details a simple proof by induction on list. Subsection 4.1 explains the inductive notion of transitive closure and the associated inductive proof principle. Subsections 4.2 and 4.3 discuss irreflexivity, representation of "finite sets" by lists, define finite restrictions of a binary relation, and detail a simple proof by induction on transitive closure. Section 5 defines paths with respect to a binary relation and proves their correspondence with transitive closure. It also defines bounded paths that are proved to preserve decidability and middle-exclusion properties of the original relation. Since bounded paths and paths are by some means equivalent on finite sets, subsection 5.4 states the intermediate result. Subsection 6.1 defines relation totality over finite sets. Subsections 6.2 to 6.5 define an acyclicity-preserving conditional single-arc addition (to a relation), and an acyclicity-preserving multi-stage arc addition over finite sets, which consists in repeating in turn single-arc addition and transitive closure. This procedure helps state linear extension equivalence in 6.6 and topological sorting equivalence in 6.7.

Convention

Let A be a Set. Throughout this paper x, y, z, and t implicitly refer to objects of type A. In the same way R, R', and R" refer to binary relations over A; l, l', and l" to lists over A, and n to natural numbers. For the sake of readability, types will sometimes be omitted according to the above convention, even in formal statements where Coq could not infer them. The notation ¬P stands for P → False, x =y for x =y → False, and ∃x, P for (∃x, P ) → False.

Preliminaries

Types and Relations

Any Coq object has a type, which informs of the usage of the object and its possible interactions with other Coq objects. The Coq syntax Obj : T means that Obj has type T. For example, f : A → B means that f requires an argument in the domain A and returns an output in the codomain B. If x has type A then f and x can be combined and yield (f x ), also written f (x ) or f x, of type The actual Coq code would need to make it clear that x and y are in A.

Definition Identity relation (x y : A) : Prop := x =y.

Excluded Middle and Decidability

The following two objects define middle-excluding equality on A and middle-excluding binary relations over A, respectively.

Definition eq midex := ∀ x y, x =y ∨ x =y.

Definition rel midex R := ∀ x y, R x y ∨ ¬R x y.

Note that the proposition eq midex is only a definition but not a theorem in Coq, i.e., there is no proof of which the conclusion is the proposition ∀ x y, x =y ∨ x =y. Same remark for rel midex.

This paper widely uses the syntax ∀ v, {B }+{C } which is a ∀ v, B ∨ C with a computational content. It means that for all v either B holds or C holds, and that, in addition, there exists a computable function expecting a v and pointing to one that holds. The next two definitions respectively say that equality on A is decidable and that a given binary relation over A is decidable.

Definition eq dec := ∀ x y, {x =y}+{x =y}.

Definition rel dec R := ∀ x y, {R x y}+{¬R x y}.

The remainder of this subsection 2.2 justifies further the syntax ∀ v, {B }+{C } as correct representation for decidability. Roughly speaking, {Obj : T | P } means the existence, with computational content, of an object of type T satisfying the predicate P, whereas ∃ Obj : T, P does the same without computational content. As shown by the two lemmas below, rel dec R is equivalent to "computable" existence of a function requiring two arguments in A and returning the boolean true if the two arguments are related or false if they are not, which amounts to decidability as discussed in subsection 1.5.

Lemma rel dec bool

: ∀ R, rel dec R → {f : A → A → bool | ∀ x y : A, if f x y then R x y else ¬R x y}. Lemma bool rel dec : ∀ R, {f : A → A → bool | ∀ x y : A, if f x y then R x y else ¬R x y} → rel dec R.
Therefore the syntax {P }+{¬P } is usually a convenient way to represent decidability in Coq. In terms of usage: while proving a proposition, both x =y ∨ x =y and {x =y}+{x =y} allow to case split (first case x =y and second case x =y). When building a function, however, only {x =y}+{x =y} allows to case split, e.g., to perform a traditional "if-then-else". It means that the computational content of {x =y}+{x =y} is stronger, as suggested below. The same kind of result is available for binary relations.

Lemma eq dec midex : eq dec → eq midex.

Lemma rel dec midex : rel dec → rel midex.

On Lists

Lists in the Coq Standard Library

All the underlying Coq code of this subsection can be found in the Coq Standard Library [START_REF]The Coq proof assistant[END_REF]. Semi-formally, lists are defined by induction as follows. Let B be any set. Consider all L complying with the following two conditions:

• nil is in L and is called the empty list over B.

• If x is in B and l is in L then (cons x l ) is in L.
The lists over B are defined as the (unique) least such an L. Formally in Coq, lists over A can be defined as follows:

Inductive list : Set := | nil : list | cons : A → list → list.
The first line defines lists over A by induction and considers the collection of all lists over A as a Set. The next line says that nil is a list over A and the last line says that applying an element of A and list over A to the constructor cons yields a new list over A. The notation x ::l stands for cons x l. Call x the head of x ::l and l its tail.

Example 1 If x and y are in A then cons x (cons y nil) is a list over A represented by x::y::nil.

In Coq, any definition by induction comes with an inductive proof principle, aka induction principle. For lists, it states that if a predicate holds for the empty list and is preserved by list construction, then it holds for all lists. Formally: ∀ (P : list → Prop), P nil → (∀ a l, P l → P (a :: l )) → ∀ l, P l.

There is a way to define functions over inductively defined objects, just along the inductive definition of those objects. This is called a definition by recursion. For example, appending two lists l and l' is defined by recursion on the first list argument l.

Fixpoint app l l' {struct l } : list := match l with | nil ⇒ l' | x :: l" ⇒ x :: app l" l' end.

The function app requires two lists over A and returns a list over A. The command Fixpoint means that app is defined by recursion and {struct l } means that the recursion involves l, the first list argument. As lists are built using two constructors, the body of the function case splits on the structure of the list argument. If it is nil then the appending function returns the second list argument. If not then the appending function returns a list involving the same appending function with a strictly smaller first list argument, which ensures process termination. The notation l ++l' stands for app l l'.

Example 2 Let x, y, z, and t be in A. Computation steps are shown below. (x::y::nil)++(z::t::nil)

x::((y::nil)++(z::t::nil)) x::y::(nil++(z::t::nil))

x::y::z::t::nil.

The function length of a list is defined by recursion, as well as the predicate In saying that a given element occurs in a given list. The predicate incl says that all the elements of a first list occur in a second list. It is defined by recursion on the first list, using In.

Decomposition of a List

If equality is middle-excluding on A and if an element occurs in a list built over A, then the list can be decomposed into three parts: a list, one occurrence of the element, and a second list where the element does not occur.

Lemma In elim right : eq midex → ∀ x l, In x l → ∃ l', ∃ l", l =l' ++(x ::l") ∧ ¬In x l".

Proof

Assume that equality is middle-excluding on A and let x be in A. Next, prove by induction on l the proposition ∀ l, In x l → ∃ l', ∃ l", l =l' ++(x ::l") ∧ ¬In x l". The base case, l =nil, is straightforward since x cannot occur in the empty list. For the inductive case, l =y::l1, the induction hypothesis is In x l1 → ∃ l', ∃ l", l1 =l' ++(x ::l") ∧ ¬In x l". Assume that x occurs in l and prove ∃ l', ∃ l", y::l1 =l' ++(x ::l") ∧ ¬In x l" as follows: case split on x occurring in l1. If x occurs in l1 then get l' and l" from the induction hypothesis, and show that y::l' and l" are witnesses. If x does not occur in l1 then x equals y, so nil and l1 are witnesses.

Repeat-Free Lists

The predicate repeat free says that no element occurs more than once in a given list. It is defined by recursion on its sole argument.

Fixpoint repeat free l : Prop := match l with | nil ⇒ True | x ::l' ⇒ ¬In x l' ∧ repeat free l' end.

a Formal and Constructive Equivalence

If equality is middle-excluding on A then a repeat free list included in another list is not longer than the other list. This is proved by induction on the repeat free list. For the inductive step, invoke In elim right to decompose the other list along the head of the repeat free list.

Lemma repeat free incl length : eq midex → ∀ l l', repeat free l → incl l l' → length l ≤length l'. Informally, the t step constructor guarantees that clos trans R contains R and the t trans constructor adds all "arcs" the absence of which would contradict transitivity.

On Relations

Intuitively The notion of subrelation helps express the induction principle for clos trans. It states that if a relation contains R and satisfies the following "weak transitivity" property then it also contains clos trans R.

∀ R', sub rel R R' → (∀ x y z, clos trans R x y → R' x y → clos trans R y z →R' y z → R' x z ) → sub rel (clos trans R) R'
The next lemma asserts that a transitive relation contains its own transitive closure (they actually coincide).

Lemma transitive sub rel clos trans

: ∀ R, transitive R → sub rel (clos trans R) R.
Proof Let R be a transitive relation over A. Prove the subrelation property by the induction principle of clos trans. The base case is trivial and the inductive case is derived from the transitivity of R.

Irreflexivity

A relation is irreflexive if no element is related to itself. Therefore irreflexivity of a relation implies irreflexivity of any subrelation.

Definition irreflexive R : Prop := ∀ x, ¬R x x. Lemma irreflexive preserved : ∀ R R', sub rel R R' → irreflexive R' → irreflexive R.

Restrictions

Throughout this paper, finite "subsets" of A are represented by lists over A. For that specific use of lists, the number and the order of occurrences of elements in a list are irrelevant. Let R be a binary relation over A and l be a list over A. The binary relation restriction R l relates elements that are both occurring in l and related by R. The predicate is restricted says that "the support of the given binary relation R is included in the list l ". And the next lemma shows that transitive closure preserves restriction to a given finite set.

Definition restriction R l x y : Prop := In x l ∧ In y l ∧ R x y.

Definition is restricted R l : Prop := ∀ x y, R x y → In x l ∧ In y l.

Lemma restricted clos trans

: ∀ R l, is restricted R l → is restricted (clos trans R) l.
Proof Assume that R is restricted to l. Let x and y in A be such that clos trans R x y, and prove by induction on that last hypothesis that x and y are in l. The base case, where "clos trans R x y comes from R x y", follows by definition of restriction. For the inductive case, where "clos trans R x y comes from clos trans R x z and clos trans R z y for some z in A", induction hypotheses are In x l ∧ In z l and In z l ∧ In y l, which allows to conclude.

If the support of a relation involves only two (possibly equal) elements, and if those two elements are related by the transitive closure, then they are also related by the original relation. By the induction principle for clos trans and lemma restricted clos trans.

Lemma clos trans restricted pair : ∀ R x y, is restricted R (x ::y::nil ) → clos trans R x y → R x y.

On Paths and Transitive Closure

Paths

The notion of path relates to one interpretation of transitive closure. Informally, a path is a list recording consecutive steps of a given relation. The following predicate says that a given list is a path between two given elements with respect to a given relation.

Fixpoint is path R x y l {struct l } : Prop := match l with | nil ⇒ R x y | z ::l' ⇒ R x z ∧ is path R z y l' end. sub rel (bounded path R n) (clos trans R).
Lemma clos trans bounded path : eq midex → ∀ R l, is restricted R l → sub rel (clos trans R) (bounded path R (length l )) .

Restriction, Decidability, and Transitive Closure

The following lemma says that it is decidable whether or not one step of a given decidable relation from a given starting point to some point z in a given finite set and one step of another given decidable relation from the same point z can lead to another given ending point. Moreover such an intermediate point z is computable when it exists, hence the syntax {z : A | . . . }.

Lemma dec lem : ∀ R' R" x y l, rel dec R' → rel dec R" → {z : A | In z l ∧ R' x z ∧ R" z y}+{ ∃ z : A, In z l ∧ R' x z ∧ R" z y}.
The following lemma is the middle-excluding version of the previous lemma.

Lemma midex lem : ∀ R' R" x y l, rel midex R' → rel midex R" → (∃ z : A, In z l ∧ R' x z ∧ R" z y) ∨ ( ∃ z : A, In z l ∧ R' x z ∧ R" z y).

Proof

By induction on l. For the inductive step, call a the head of l. Then case split on the induction hypothesis. In the case of existence, any witness for the induction hypothesis is also a witness for the wanted property. In the case of non-existence, case split on R' x a and R" a y.

By unfolding the definition rel midex, the next result implies that given a restricted and middle-excluding relation, a given natural number and two given points, either there is a path of length at most that number between those points or there is no such path. Replacing midex by dec in the lemma yields a correct lemma about decidability.

Lemma bounded path midex : ∀ R l n, is restricted R l → rel midex R → rel midex (bounded path R n).
Proof First prove three simple lemmas relating bounded path, n, and S n. Then let R be a middle-excluding relation restricted to l and x and y be in A. Perform an induction on n. For the inductive step, case split on the induction hypothesis with x and y. If bounded path R n x y holds then it is straightforward. If its negation holds then case split on em lem with R, bounded path R n, x, y, and l. In the existence case, just notice that a path of length less than n is of length less than S n. In the non-existence case, show the negation of bounded path in the wanted property.

Let equality and a restricted relation be middle-excluding over A, then the transitive closure of the relation is also middle-excluding. The proof invokes bounded path midex, bounded path clos trans, and clos trans bounded path. The decidability version of it is also correct.

Lemma restricted midex clos trans midex : eq midex → ∀ R l, rel midex R → is restricted R l → rel midex (clos trans R).

Intermediate Results

The following theorems state the equivalence between decidability of a relation and uniform decidability of the transitive closures of its finite restrictions. The first result invokes clos trans restricted pair and the second implication uses restricted dec clos trans dec. Note that decidable equality is required only for the second implication. These results remain correct when considering excluded middle instead of decidability.

Theorem clos trans restriction dec R dec : ∀ R (∀ l, rel dec (clos trans (restriction R l ))) → rel dec R.

Theorem R dec clos trans restriction dec : eq dec → ∀ R rel dec R → ∀ l, rel dec (clos trans (restriction R l )).

Linear Extension and Topological Sorting

Consider R a binary relation over A and l a list over A. This section presents a way of preserving acyclicity of R while "adding arcs" to the restriction of R to l in order to build a total and transitive relation over l. In particular, if R is acyclic, then its image by the relation completion procedure must be a strict total order. The basic idea is to compute the transitive closure of the restriction of R to l, add an arc iff it can be done without creating any cycle, taking the transitive closure, adding an arc if possible, etc. All those steps preserve existing arcs. Since l is finite, there are finitely many eligible arcs, which ensures termination of the process. This is not the fastest topological sort algorithm but its fairly simple expression leads to a simple proof of correctness.

Total

R is said to be total on l if any two distinct elements in l are related either way. Such a trichotomy property for a relation implies trichotomy for any bigger relation.

Definition trichotomy R x y : Prop := R x y ∨ x =y ∨ R y x.

Definition total R l : Prop := ∀ x y, In x l → In y l → trichotomy R x y.

Lemma trichotomy preserved : ∀ R R' x y, sub rel R R' → trichotomy R x y → trichotomy R' x y.

Try Add Arc

If x and y are equal or related either way then define the relation try add arc R x y as R, otherwise define it as the disjoint union of R and the arc (x,y).

Inductive try add arc R x y : A → A → Prop := | keep : ∀ z t, R z t → try add arc R x y z t | try add : x =y → ¬R y x → try add arc R x y x y.

Prove by induction on l and a few case splittings that, under some conditions, a path with respect to an image of try add arc is also a path with respect to the original relation.

Lemma path try add arc path : ∀ R t x y l z, ¬(x =z ∨ In x l ) ∨ ¬(y=t ∨ In y l ) → is path R (try add arc R x y) z t l → is path R z t l.

The next three lemmas lead to the conclusion that the function try add arc does not create cycles. The first one is derived from a few case splittings and the last one highly relies on the second one but also invokes clos trans path.

Lemma trans try add arc sym : ∀ R x y z t, transitive R → try add arc R x y z t → try add arc R x y t z → R z z.

Lemma trans bounded path try add arc : eq midex → ∀ R x y z n, transitive R → bounded path (try add arc R x y ) n z z → R z z.

Proof

By induction on n. The base case requires only trans try add arc sym. For the inductive case, consider a path of length less than or equal to n+1 and build one of length less than n+1 as follows. By path repeat free length the path may be repeat free, i.e., without circuit. Proceed by case splitting on the construction of the path: when the path is nil, it is straightforward. If the length of the path is one then invoke sub rel try add arc trans try add arc sym; otherwise perform a 4-case splitting (induced by the disjunctive definition of try add arc) on the first two (try add arc R x y)-steps of the path. Two cases out of the four need lemmas transitive sub rel clos trans, path clos trans, and path try add arc path.

Lemma try add arc irrefl : eq midex → ∀ R x y, transitive R → irreflexive R → irreflexive (clos trans (try add arc R x y)).

Try Add Arc (One to Many)

The function try add arc one to many recursively tries to (by preserving acyclicity) add all arcs starting at a given point and ending in a given list.

Fixpoint try add arc one to many R x l {struct l } : A → A → Prop := match l with | nil ⇒ R | y::l' ⇒ clos trans (try add arc (try add arc one to many R x l' ) x y) end.

The following three lemmas prove preservation properties about the function try add arc one to many: namely, arc preservation, restriction preservation, and middle-exclusion preservation. Decidability preservation is also correct, although not formally stated here.

Lemma sub rel try add arc one to many : ∀ R x l, sub rel R (try add arc one to many R x l ).

Proof By induction on l. For the inductive step, call a the head of l and l' its tail. Use transitivity of sub rel with try add arc one to many x l' and try add arc (try add arc one to many x l' ) x a. Also invoke clos trans and a similar arc preservation property for try add arc.

Lemma restricted try add arc one to many : ∀ R l x l', In x l → incl l' l → is restricted R l → is restricted (try add arc one to many R x l' ) l.

Proof By induction on l', restricted clos trans, and a similar restriction preservation property for try add arc.

Definition non uni topo sortable R := ∀ l, ∃ R' : A → A → bool, linear extension R l (fun x y ⇒ R' x y=true).

In the definition above, R' represents a decidable binary relation that intends to be a linear extension of R over the list l. But R' has type A → A → bool so it cannot be used with the predicate linear extension R l that expects an object of type A → A → Prop, which is the usual type for representing binary relations in Coq. The function fun x y ⇒ (R' x y)=true above is the translation of R' in the suitable type/representation. It expects two elements x and y in A and returns the proposition R' x y=true, in Prop.

In this article, a given relation over A is said to be sortable if there exists a computable function expecting a list over A and producing, over the list argument, a (decidable) linear extension of the original relation.

Definition uni topo sortable R := {F : list A → A → A → bool | ∀ l, linear extension R l (fun x y ⇒ (F l x y)=true )}.
The third definition of topological sort uses the concept of asymmetry, which is now informally introduced; from an algorithmic viewpoint: given a way of representing binary relations, different objects may represent the same binary relation; from a logical viewpoint: two binary relations different in intension, i.e. their definitions intend different things, may still coincide, i.e. may be logically equivalent. In an arbitrary topological sort algorithm, the returned linear extension may depend on which object has been chosen to represent the original binary relation. For example, applying the empty relation on a given two-element set to a topological sort algorithm may produce the two possible linear extensions depending on the order in which the two elements constituting the set are given. This remark leads to the following definition.

Definition asym R G := ∀ x y : A, x =y → ¬R x y → ¬R y x → ¬(G (x ::y::nil ) x y ∧ G (y::x ::nil ) x y).

Next comes the definition of asymmetry for a topological sort of a binary relation. The syntax let variable:= formula in formula' avoids writing formula several times in formula'.

Definition asym topo sortable R := {F

: list A → A → A → bool | let G:= (fun l x y ⇒ F l x y=true) in asym R G ∧ ∀ l, linear extension R l (G l )}.
Given a binary relation R over A, the remainder of this subsection proves that the four following assertions are equivalent:

1. Equality on A is decidable, and R is decidable and acyclic.

2. R is middle-excluding and asymmetrically sortable.

3. R is decidable and uniformly sortable.

Equality on

A is decidable, and R is decidable and non-uniformly sortable.

The following lemma says that if there exists a computable function expecting a list over A and producing a (decidable) strict total order over A, then equality on A is decidable. The proof is similar to the one for total order eq midex.

Lemma total order eq dec :

{F : list A → A → A → bool | ∀ l, let G := fun x y ⇒ F l x y=true in transitive A G ∧ irreflexive G ∧ total G l } → eq dec A.
Next lemma shows that LETS yields asymmetric topological sort.

Lemma LETS asym : ∀ R, asym R (LETS R).

Proof Assume all possible premises, especially let x and y be in A. As a preliminary: the hypotheses involve one relation image of restriction and four relations images of try add arc. Prove that all of them are restricted to x ::y::nil. Then perform a few cases splittings and apply clos trans restricted pair seven times.

The quadruple equivalence claimed above is derived from rel dec midex and the six theorems below. The proofs are rather similar to the middle-excluding case in subsection 6.6. The first theorem proves 1 → 2 by the relevant lemmas of subsection 6.5 and LETS producing a witness for the computational existence. The second (straightforward) and the third show 2 → 3. The fourth (straightforward) and the fifth, proved by total order eq dec, yield 3 → 4. The last shows 4 → 1 by invoking local global acyclic.

Theorem possible asym topo sorting : ∀ R, eq dec A → rel dec R → irreflexive (clos trans A R) → asym topo sortable R.

Theorem asym topo sortable uni topo sortable : ∀ R, asym topo sortable R → uni topo sortable R.

Theorem asym topo sortable rel dec : ∀ R, rel midex R → asym topo sortable R → rel dec R.

Proof

First notice that R is acyclic by local global acyclic and that equality on A is decidable by total order eq dec. Then let x and y by in A. By decidable equality, case split on x and y being equal. If they are equal then they are not related by acyclicity. Now consider that they are distinct. Thanks to the assumption, get TS an asymmetric topological sort of R. Case split on x and y being related by TS (x ::y::nil ). If they are not then they cannot be related by R by subrelation property. If they are related then case split again on x and y being related by TS (y::x ::nil ). If they are not then they cannot be related by R by subrelation property. If they are then they also are by R by the asymmetry property.

Theorem uni topo sortable non uni topo sortable : ∀ R, uni topo sortable R → non uni topo sortable R.

Theorem rel dec uni topo sortable eq dec : ∀ R, rel dec R → uni topo sortable R → eq dec A.

Theorem rel dec non uni topo sortable acyclic : ∀ R, rel dec R → non uni topo sortable R → irreflexive (clos trans A R).

Conclusion

This paper has given a detailed account on a few facts related to linear extensions of acyclic binary relations. The discussion is based on a formal proof developed with the proof assistant Coq. Since arguments are constructive, they are also correct with respect to traditional mathematical reasoning. The paper aimes to be understandable to mathematicians new to Coq or more generally by readers unfamiliar with constructive issues. The three main results are stated again below. First, a binary relation over a set with decidable/middle-excluding equality is decidable/middle-excluding iff transitive closures of its finite restrictions are also decidable/middle-excluding. This theorem is involved in the proof of the second and third main results. Second, consider a middle-excluding relation over an arbitrary domain. It is acyclic and equality on its domain is middle-excluding iff any of its finite restriction has a middle-excluding linear extension. Third, consider R a decidable binary relation over A. The following three propositions are equivalent:

• Equality on A is decidable and R is acyclic.

• Equality on A is decidable and R is non-uniformly sortable.

• R is uniformly sortable.

The proofs of the last two main results rely on the constructive function LETS that is actually (similar to) a basic topological sort algorithm. An effective program could therefore be extracted from the Coq development (related to computability). The original proof would in turn serve as a formal proof of correctness for the program.

4. 1

 1 Transitive Closure in the Coq Standard Library Traditionally, the transitive closure of a binary relation is the smallest transitive binary relation including the original relation. The notion of transitive closure can be formally defined by induction, in the Coq Standard Library. The following function clos trans expects a relation over A and yields its transitive closure, which is also a relation over A. Inductive clos trans R : A → A → Prop := | t step : ∀ x y, R x y → clos trans R x y | t trans : ∀ x y z, clos trans R x y → clos trans R y z → clos trans R x z.

  , two elements are related by the transitive closure of a binary relation if one can start at the first element and reach the second one in finitely many steps of the original relation. Therefore replacing clos trans R x y → clos trans R y z → clos trans R x z by R x y → clos trans R y z → clos trans R x z or clos trans R x y → R y z → clos trans R x z in the definition of clos trans would yield two relations coinciding with clos trans. Those three relations are yet different in intension: only clos trans captures the meaning of the terminology "transitive closure". The Coq Standard Library also defines what a transitive relation is. In addition, this paper needs the notion of subrelation. Definition sub rel R R' : Prop := ∀ x y, R x y → R' x y.

  Both the collection of all natural numbers and the collection of the two booleans true and false have type Set. Intuitively, proving propositions in Prop amounts to traditional (and intuitionistic) mathematical reasoning as proving objects in Set is computationally stronger since effective programs can be extracted from theorems in Set. Now consider g : A → (B → C ) where the parentheses are usually omitted by convention. The function g expects an argument in A and returns a function expecting an argument in B and returning an output in C. Therefore g can be seen as a function requiring a first argument in A, a second one in B, and returning an object in C. Binary relations over A can be represented by functions typed in A → A → Prop, i.e. requiring two arguments in A and returning a proposition (that may be interpreted as "the two arguments are related"). The returned proposition may be True, False, or something else that may or may not be equivalent to either True or False. For example if it returns always something absurd, i.e., implying False, then it is "the" empty relation over A. The object Identity relation, defined below in the light Coq formalism using this paper's convention, can be interpreted as the identity relation over A. Indeed, it requires two arguments in A and returns a proposition asserting that those arguments are equal.

B. A type is also a Coq object so it has a type too. The only types of types mentioned in this paper are Prop and Set. The two propositions True and False are in Prop but in a constructive setting there are propositions, i.e., objects in Prop, neither equivalent to True nor to False. Definition Identity relation x y : Prop := x =y.

Acknowledgement

I thank Pierre Lescanne for his careful reading and helpful comments, as well as Philippe Audebaud, Guillaume Melquiond, and Victor Poupet for discussions, and Jingdi Zeng for proofreading my English.

a Formal and Constructive Equivalence

The following two lemmas show the correspondence between paths and transitive closure. The first is proved by the induction principle of clos trans and an appending property on paths proved by induction on lists. For the second, let y be in A and prove ∀ l x, is path R x y l → clos trans R x y by induction on l. Now consider the variable appearance order ∀ y l x in this lemma. Changing the order would yield a correct lemma as well, but the proof would be less workable. Indeed y can be fixed once for all but x needs to be universally quantified in the induction hypothesis, so x must appear after l on which the induction is performed. Also note that the two lemmas imply ∀ x y, clos trans R x y ↔ ∃ l, is path R x y l.

Lemma clos trans path : ∀ x y, clos trans R x y → ∃ l, is path R x y l.

Lemma path clos trans : ∀ y l x, is path R x y l → clos trans R x y.

Assume that equality is middle-excluding on A and consider a path between two points. Between those two points there is a repeat free path avoiding them and (point-wise) included in the first path. The inclusion is also arc-wise by construction, but it is not needed in this paper.

Lemma path repeat free length :

Proof

Assume that equality is middle-excluding on A, let y be in A, and perform an induction on l. For the inductive step, call a the head of l. If a equals y then the empty list is a witness for the existential quantifier. Now assume that a and y are distinct. Use the induction hypothesis with a and get a list l'. Case split on x occurring in l'. If x occurs in l' then invoke lemma In elim right and decompose l' along x, and get two lists. In order to prove that the second list, where x does not occur, is a witness for the existential quantifier, notice that splitting a path yields two paths (a priori between different elements) and that appending reflects the repeat free predicate (if the appending of two lists is repeat free then the original lists also are). Next, assume that x does not occur in l'. If x equals a then l' is a witness for the existential quantifier. If x and a are distinct then a::l' is a witness.

Bounded Paths

Given a relation and a natural number, the function bounded path returns a relation saying that there exists a path of length at most the given natural number between two given elements.

Inductive bounded path R n :

Below, two lemmas relate bounded path and clos trans. The first one is derived from path clos trans; the second one from clos trans path, path repeat free length, repeat free incl length, and a path of a restricted relation being included in the support of the relation. Especially, the second lemma says that in order to know whether two elements are related by the transitive closure of a restricted relation, it suffices to check whether there is, between those two elements, a path of length at most the "cardinal" of the support of the relation.

Lemma bounded path clos trans : ∀ R n, a Formal and Constructive Equivalence

Lemma try add arc one to many midex : eq midex → ∀ R x l l', In x l → incl l' l → is restricted R l → rel midex R → rel midex (try add arc one to many R x l' ).

Proof

By induction on l'. Also invoke restricted try add arc one to many, lemma restricted midex clos trans midex with l, and a similar middle-exclusion preservation property for try add arc.

Next, a step towards totality.

Lemma try add arc one to many trichotomy : eq midex → ∀ R x y l l', In y l' → In x l → incl l' l → is restricted R l → rel midex R → trichotomy (try add arc one to many R x l' ) x y.

Proof

By induction on l'. For the inductive step, invoke trichotomy preserved, case split on y being the head of l' or y occurring in the tail of l'. Also refer to a similar trichotomy property for try add arc.

Try Add Arc (Many to Many)

The function try add arc many to many requires a relation and two lists. Then, using try add arc one to many, it recursively tries to safely add all arcs starting in first list argument and ending in the second one.

Fixpoint try add arc many to many R l' l {struct l' } : A → A → Prop := match l' with | nil ⇒ R | x ::l" ⇒ try add arc one to many (try add arc many to many R l" l ) x l end.

The following three results proved by induction on the list l' state arc, restriction, and decidability preservation properties of try add arc many to many. For the inductive case of the first lemma, call l"the tail of l', apply the transitivity of sub rel with (try add arc many to many R l"l ), and invoke lemma sub rel try add arc one to many. Use restricted try add arc one to many for the second lemma. For the third one invoketry add arc one to many dec and also restricted try add arc many to many. Middle-exclusion preservation is also correct, although not formally stated here.

Lemma sub rel try add arc many to many : ∀ R l l', sub rel R (try add arc many to many R l' l ).

Lemma restricted try add arc many to many : ∀ R l l', incl l' l → is restricted R l → is restricted (try add arc many to many R l' l ) l.

Lemma try add arc many to many dec : → ∀ R l l', incl l' l → is restricted R l → rel dec R → rel dec (try add arc many to many R l' l ).

The next two results state a trichotomy property and that the function try add arc many to many does not create any cycle.

Lemma try add arc many to many trichotomy : eq midex → ∀ R l x y l', incl l' l → In y l → In x l' → restricted R l → rel midex R → trichotomy (try add arc many to many R l' l ) x y.

Proof By induction on l'. Start the inductive step by case splitting on x being the head of l' or occurring in its tail l". Conclude the first case by try add arc one to many trichotomy, try add arc many to many midex, and restricted try add arc many to many. Use trichotomy preserved, the induction hypothesis, and sub rel try add arc one to many for the second case.

Lemma try add arc many to many irrefl : eq midex → ∀ R l l', incl l' l → is restricted R l → transitive A R → irreflexive R → irreflexive (try add arc many to many R l' l ).

Proof By induction on l'. For the inductive step, first prove a similar irreflexivity property for try add arc one to many by induction on lists and try add arc irrefl. Then invoke restricted try add arc many to many. Both this proof and the one for try add arc one to many also require transitivity of the transitive closure and an additional case splitting on l' being nil or not.

Linear Extension/Topological Sort Function

Consider the restriction of a given relation to a given list. The following function tries to add all arcs both starting and ending in that list to that restriction while still preserving acyclicity.

Definition LETS R l : A → A → Prop := try add arc many to many (clos trans (restriction R l )) l l.

The next three lemmas are proved by sub rel try add arc many to many, transitive clos trans, and restricted try add arc many to many respectively.

Lemma LETS sub rel : ∀ R l, sub rel (clos trans (restriction R l )) (LETS R l ).

Lemma LETS transitive : ∀ R l, transitive (LETS R l ).

Under middle-excluding equality, the finite restriction of R to l has no cycle iff LETS R l is irreflexive. Prove left to right by try add arc many to many irrefl, and right to left by irreflexive preserved and LETS sub rel.

If R and equality on A are middle-excluding then LETS R l is total on l. This is proved by R midex clos trans restriction midex (in 5.4 ) and try add arc many to many trichotomy.

The next two lemmas show that if R and equality on A are middle-excluding (resp. decidable) then so is LETS R l : by try add arc many to many midex (resp. try add arc many to many dec) and R midex clos trans restriction midex (resp. R dec clos trans restriction dec).

Lemma LETS dec : eq dec → ∀ R, rel dec R → ∀ l, rel dec (LETS R l ).

a Formal and Constructive Equivalence

Linear Extension

Traditionally, a linear extension of a partial order is a total order including the partial order. Below, a linear extension (over a list) of a binary relation is a strict total order (over the list) that is bigger than the original relation (restricted to the list).

The next two lemmas say that a relation "locally" contained in some acyclic relation is "globally" acyclic and that if for any list over A there is a middle-excluding total order over that list, then equality is middle-excluding on A.

Lemma local global acyclic

Proof

Let R be a relation over A. Assume that any finite restriction of R is included in some strict partial order. Let x be in A such that clos trans R x x. Then derive False as follows. Invoke clos trans path and get a path. It is still a path for the restriction of R to the path itself (the path is a list seen as a subset of A). Use path clos trans, then the main assumption, transitive sub rel clos trans, and the monotonicity of clos trans with respect to sub rel.

Lemma total order eq midex :

Proof

Assume the left conjunct, let x and y be in A, use the assumption with x ::y::nil, get a relation, and double case split on x and y being related either way.

Consider a middle-excluding relation on A. It is acyclic and equality is middle-excluding on A iff for any list over A there exists, on the given list, a decidable strict total order containing the original relation.

Theorem linearly extendable

Proof Left to right: by the relevant lemmas of subsection 6.5, (LETS R l ) is a witness for the existential quantifier. Right to left by local global acyclic and total order eq midex.

Topological Sorting

In this subsection, excluded-middle results of subsection 6.6 are translated into decidability results and augmented: as there is only one concept of linear extension in subsection 6.6, this section presents three slightly different concepts of topological sort. Instead of the equivalence of theorem linearly extendable, those three definitions yield a quadruple equivalence.

From now on a decidable relation may be represented by a function to booleans instead of a function to Prop satisfying the definition rel dec. However, those two representations are "equivalent" thanks to lemmas rel dec bool and bool rel dec in subsection 2.2.

In this article, a given relation over A is said to be non-uniformly (topologically) sortable if the restriction of the relation to any list has a decidable linear extension.