Reuven Cohen
email: cohenr@bu.edu

Pierre Fraigniaud
email: pierre@liafa.jussieu.fr.

David Ilcinkas
email: david.ilcinkas@labri.fr.

Amos Korman
email: amos.korman@liafa.jussieu.fr.

David Peleg
email: david.peleg@weizmann.ac.il.

Label-Guided Graph Exploration by a Finite Automaton

Keywords: C.2.1 [Computer-communication networks]: Network Architecture and Design, C.2.2 [Computer-communication networks]: Network Protocols, C.2.4 [Computer-communication networks]: Distributed Systems, E.1 [Data Structures]: Distributed data structures, Graphs and networks, G.2.1 [Discrete mathematics]: Combinatorics, G.2.2 [Discrete mathematics]: Graph theory Algorithms, Theory Distributed algorithms, Graph exploration, Labeling schemes

published or not. The documents may come

L'archive ouverte

Label-Guided Graph Exploration by a Finite Automaton

This paper concerns graph exploration by finite automata. Let R be a finite automaton, simply referred to in this context as a robot, moving in an unknown undirected graph G = (V, E). The robot has no a priori information about the topology of G and its size. To allow the robot R to distinguish between the different edges of a node u while visiting it, the d = deg(u) edges incident to u are associated with d distinct port numbers in {0, . . . , d -1}, in a one-to-one manner. The port numbering is given as part of the input graph, and the robot has no a priori information about it. For convenience of terminology, we henceforth refer to the edge incident to port number l at node u simply as "edge l of u". (Clearly, if this edge connects u to v, then it may also be referred to as "edge l ′ of v" for the appropriate l ′ .) The robot has a finite number of states and a transition function f . If R enters a node of degree d through port i in state s, then it switches to state s ′ and exits the node through port i ′ , where (s ′ , i ′ ) = f (s, i, d). The objective of the robot is to explore the graph, i.e., to visit all its nodes. The size of the robot's memory equals the logarithm of the number of states.

The first known algorithm designed for graph exploration was introduced by Shannon [START_REF] Shannon | Presentation of a maze-solving machine[END_REF]. Since then, several papers have been dedicated to the feasibility of graph exploration by a finite automaton. Rabin [START_REF] Rabin | Maze threading automata[END_REF]] conjectured that no finite automaton with a finite number of indistinguishable pebbles can explore all graphs (a pebble is a marker that can be dropped at and removed from nodes). The first step towards a formal proof of Rabin's conjecture is generally attributed to Budach [START_REF] Budach | Automata and labyrinths[END_REF], for a robot without pebbles. Blum and Kozen [START_REF] Blum | On the power of the compass (or, why mazes are easier to search than graphs)[END_REF]] improved Budach's result by proving that a robot with three pebbles cannot perform exploration of all graphs. Kozen [START_REF] Kozen | Automata and planar graphs[END_REF] proved that a robot with four pebbles cannot explore all graphs. Finally, Rollik [START_REF] Rollik | Automaten in planaren Graphen[END_REF]] gave a complete proof of Rabin's conjecture, showing that no robot with a finite number of pebbles can explore all graphs. The result holds even when restricted to planar 3-regular graphs. Without pebbles, it was proved [Fraigniaud et al., 2005] that a robot needs Θ(D log ∆) bits of memory for exploring all graphs of diameter D and maximum degree ∆. On the other hand, if the class of input graphs is restricted to trees, then exploration is possible even by a robot with no memory (i.e., zero states), simply by depth-first search (DFS) using the transition function f (i, d) = i + 1 mod d (see, e.g., [START_REF] Diks | Tree Exploration with Little Memory[END_REF]).

Two variants of the exploration problem have been addressed in the literature: exploration with stop (in which the robot has to complete exploration and eventually stop) and exploration with return (in which the robot has to perform exploration and return to its starting position). It is shown in [START_REF] Diks | Tree Exploration with Little Memory[END_REF]] that exploration

• 113 with stop of n-node trees requires a robot with memory size Ω(log log log n) bits, and in [START_REF] Gasieniec | Tree exploration with logarithmic memory[END_REF] that exploration with return of n-node trees can be achieved by a robot with O(log n) memory bits. It is impossible to explore arbitrary graphs with stop by a single robot if no marking of nodes is allowed. In [Fraigniaud et al., 2005], the authors show that also using one pebble, the exploration with stop of n-node graphs requires a robot with memory size Ω(log n) bits.

Label-guided exploration:

The ability of dropping and removing pebbles at nodes can be viewed alternatively as the ability of the robot to dynamically label the nodes. If the robot is given k pebbles, then at any time during the exploration, u∈V |l u | ≤ k, where l u is the label of node u and |l u | denotes the size of the label in unary.

In certain settings, it is expected that the graph will be visited by many exploring robots, and consequently, it is desired to preprocess the graph by leaving fixed (preferably small) road-signs, or labels, that will aid the robots in their exploration task. As a possible scenario, one may consider a network system where finite automata are used for traversing the system and distributing information in a sequential manner. Recently, a number of papers studied the affects of assigning (short) labels in a preprocessing stage, in order to ease a distributed task (e.g., [START_REF] Korman | Proof Labeling Schemes[END_REF][START_REF] Fraigniaud | Oracle size: a new measure of difficulty for communication tasks[END_REF][START_REF] Fraigniaud | Local MST Computation with Short Advice[END_REF]). This paper considers the affects of allowing the system designer to assign labels to the nodes in a preprocessing stage, and using these labels to guide robot explorations. The transition function f is augmented to utilize labels as follows. If the robot R in state s enters a node of degree d, labeled by l, through port i, then it switches to state s ′ and exits the node through port i ′ , where

(s ′ , i ′ ) = f (s, i, d, l).
This model can be considered stronger than Rabin's pebble model since labels are given in a preprocessing stage, but it can also be considered weaker since, once assigned to nodes, the labels cannot be modified. Remark. It should be noted that the general function f presented here may depend on d, i and l, all of which may require log n bits to be described in an n-node graph. However, our formalism fits in the standard context of Mealy automata, i.e., the number of states of the robot is independent from the sizes of the inputs and outputs of the transition function. In contrast, for Moore automata, the output of the transition function is a state, in which the output port number is encoded, and thus the number of states of a Moore automaton is at least the degree of the graph. Nevertheless, the algorithm described in this paper actually deals with only three possible outputs: i ′ = i, i ′ = i + 1 mod d, and i ′ = i -1 mod d, which can be interpreted as "go back", "go clockwise", and "go counterclockwise" commands, respectively. Therefore, the algorithm can be executed by a Moore automaton in contexts for which a natural spacial orientation does exist, as, e.g., for robots moving in a physical environment.

We address the design of exploration labeling schemes. Such schemes consist of a pair (L, R) such that, given any graph G with any port numbering, the algorithm L labels the nodes of G, and the robot R explores G with the help of the labeling produced by L. In particular, we are interested in exploration labeling schemes for which: (1) the preprocessing time required to label the nodes is polynomial, (2) the labels are short, and (3) the exploration is completed after a small number of edge traversals.

Our results:

As a consequence of Rollik's result, any exploration labeling scheme must use at least two different labels. Our main result states that just three labels (e.g., three colors) are sufficient for enabling a robot (with constant-size memory) to explore all graphs. Moreover, we show that our labeling scheme gives to the robot the power to stop once exploration is completed, although, in the general setting of graph exploration, the robot is not required to stop once the exploration has been completed, i.e., once all nodes have been visited. In fact, we show that exploration is completed in time O(m), i.e., after O(m) edge traversals, in any m-edge graph. In addition, we prove that the node-labeling can be done online while the robot is exploring the graph. The completion time of the algorithm then becomes O(Dm), where D is the diameter of the graph.

For the class of bounded degree graphs, we design an exploration scheme using even smaller labels. More precisely, we show that just two labels (i.e., 1-bit labels) are sufficient for enabling a robot to explore all bounded degree graphs. The robot is however required to have a memory of size O(log ∆) to explore all graphs of maximum degree ∆. The completion time O(∆ O(1) m) of the exploration is larger than the one of our previous 2-bit labeling scheme, nevertheless it remains polynomial.

All these results are summarized in Table I. The two mentioned labeling schemes require polynomial preprocessing time.

Label size

Robot's memory Time (#bits)

(#bits) (# edge traversals) 2 O(1) O(m) 1 O(log ∆) O(∆ O(1) m)
Table I. Summary of main results.

We also prove several impossibility results for 1-state (i.e., oblivious) robots. The behavior of 1-state robots depends solely on the input port number, and on the degree and label of the current node. In particular, we prove that for any d > 4 and for any 1-state robot using at most ⌊log d⌋-2 colors, there exists a simple graph of maximum degree d that cannot be explored by the robot. This lower bound on the number of colors needed for exploration can be increased exponentially to d/2-1 by allowing loops.

A 2-BIT EXPLORATION-LABELING SCHEME

Exploration with pre-labeling

In this section, we describe an exploration-labeling scheme using only 2-bit (actually, 3-valued) labels. More precisely, we prove the following.

Theorem 2.1. There exists a robot with less than 25 states satisfaying the property that for any m-edge graph G, it is possible to color the nodes of G with three

• 115 colors (or alternatively, assign each node a 2-bit label) so that using the labeling, the robot can explore the graph G, starting from any given node and terminating after identifying that the entire graph has been traversed. Moreover, the total number of edge traversals by the robot is at most 20m.

To prove Theorem 2.1, we first describe the labeling scheme L and then the exploration algorithm. The node labeling is in fact very simple, and uses three colors denoted white, black, and red. Let D denote the diameter of the graph.

Labeling L.. Pick an arbitrary node r to be the root of the labeling L. Nodes at distance d from r, 0 ≤ d ≤ D, are labeled white if d mod 3 = 0, black if d mod 3 = 1, and red if d mod 3 = 2.

The neighbor set N (u) of each node u can be partitioned into three disjoint sets: (1) the set pred(u) of neighbors closer to r than u; (2) the set succ(u) of neighbors farther from r than u; (3) the set sibling(u) of neighbors at the same distance from r as u. We also identify the following two special subsets of neighbors:

-parent(u) is the node v ∈ pred(u) such that the edge {u, v} has the smallest port number at u among all edges connecting it to a node in pred(u). -child(u) is the set of nodes v ∈ succ(u) such that parent(v) = u.

For the root, set parent(r) = ∅. The exploration algorithm is partially based on the following observations.

(1) For the root r, child(r) = succ(r) = N (r).

(2) For every node u with label L(u), and for every neighbor v ∈ N (u), the label L(v) uniquely determines whether v belongs to pred(u), succ(u) or sibling(u).

(3) Once at node u, a robot can identify parent(u) by visiting its neighbors successively, starting with the neighbor connected to port 0, then port 1, and so on. Indeed, by observation 2, the nodes in pred(u) can be identified by their label.

The order in which the robot visits the neighbors ensures that parent(u) is the first visited node in pred(u).

Observe that one of the main difficulties of graph exploration by a robot with a finite memory is that the robot entering some node u by port p, and aiming at exiting u by the same port p after having performed some local exploration around u, does not have enough memory to store the value of p.

The Robot R.. The overall exploration performed by our algorithm is the DFS of the spanning tree defined by the parent function (and child function). However, it is not always possible to know if an edge {u, v} belongs to this spanning tree, based solely on the colors of u and v. To solve this problem, our exploration algorithm uses a procedure called Check Edge. This procedure is specified as follows. When Check Edge(j) is initiated at some node u, the robot starts visiting the neighbors of u one by one, and eventually returns to u by the same edge j reporting one of three possible outcomes: "child", "parent", or "false". These values have the following interpretation:

(i). if "child" is returned, then edge j at u leads to a child of u; (ii). if "parent" is returned, then edge j at u leads to the parent of u;

• Reuven Cohen et al.

(iii). if "false" is returned, then edge j at u leads to a node in N (u)\(parent(u)∪ child(u)).

The implementation of Procedure Check Edge will be described later. Meanwhile, let us describe how the algorithm makes use of this procedure to perform exploration. In this description, all arithmetic operations are modulo d.

Assume that the robot R is initially at the root r of the 3-coloring L of the nodes. R leaves r by port number 0, in state down. Note that, by the above observations, the node at the other endpoint of edge 0 of r is a child of r.

Now assume that R enters a node u of degree d via port number i. If R is in state down, then it aims at identifying a child of u if one exists, or to backtrack along edge i of u if none exists. If R is in state up, then it aims at identifying a child of u with port number j ∈ {i + 1, . . . , p -1} if one exists (where p is the port number of the edge leading to parent(u)), or to carry on moving up to the parent of u if there is no such child. In both cases, R achieves its goal as follows. R executes Procedure Check Edge(j) for every port number j = i + 1, i + 2, . . . until the procedure eventually returns "child" or "parent" for some port number j. R then sets its state to down in the former case and up in the latter, and leaves u by port j.

If the robot does not start from the root r of the labeling L, then it first goes to r by using Procedure Check Edge to identify the parent of every intermediate node, and by identifying r as the only node with pred(r) = ∅.

Moreover, the robot can stop after the exploration has been completed. More precisely, this can be done by introducing a slight modification of the robot behavior when it enters a node u of degree d via port number d -1 in state up. In this case, R first checks whether u has a parent. If yes, then it acts as previously stated (R does not need to store d since d is the node degree). If not, the robot terminates the exploration.

Procedure Check Edge.. We now describe the actions of the robot R when Procedure Check Edge(j) is initiated at a node u. The objective of R is to set the value of the variable edge to one of {parent, child, false}. We denote by v the other endpoint of the edge e with port number j at u. First, R moves to v in state "check edge", carrying with it the color of node u. Let i be the port number of edge e at v. There are three cases to be considered.

(a) v ∈ sibling(u):. Then R backtracks through port i and reports "edge = false". (b) v ∈ pred(u):. Then R aims at checking whether v is the parent of u, that is, whether u is a child of v. For that purpose, R moves back to u, and proceeds as follows: R successively visits edges j -1, j -2, . . . of u until either the other endpoint of the edge belongs to pred(u), or all edges j -1, j -2, . . . , 0 have been visited. R then sets "edge=false" in the former case and "edge=parent" in the latter. At this point, let k be the port number at u of the last edge visited by R. Then R successively visits edges k + 1, k + 2, • • • until the other endpoint belongs to pred(u). Then it moves back to u and reports the value of edge.

(c) v ∈ succ(u):. Then R aims at checking whether u is the parent of v. For that purpose, R proceeds in a way similar to Case (b), i.e., it successively visits edges i -1, i -2, . . . of v until either the other endpoint of the edge belongs to pred(v), or

• 117 all edges i -1, i -2, . . . , 0 have been visited. R then sets its variable edge to "false" in the former case and to "child" in the latter. At this point of the exploration, let k denote the port number of the last edge incident to v that R visited. Then R successively visits edges k + 1, k + 2, . . . until the other endpoint w of the edge belongs to pred(v). Then it moves to w and reports the value of edge.

This completes the description of our exploration procedure.

Proof of Theorem 2.1:

Clearly, all nodes of an m-edge graph can be labelled by L, using two bits per label, in time linear in m. It remains to prove the correctness of the exploration algorithm.

It is easy to check that if Procedure Check Edge satisfies its specifications, then the robot R essentially performs a DFS traversal of the graph using edges {u, v} where u = parent(v) or u ∈ child(v). Thus, we focus on the correctness of Procedure Check Edge(j) initiated at node u. Let v be the other endpoint of the edge e with port number j at u, and let i be the port number of edge e at v. We check separately the three cases considered in the description of the procedure. By the previous observations, comparing the color of the current node v with the color of u allows R to distinguish between these cases.

If v ∈ sibling(u), then v is neither a parent nor a child of u, and thus reporting "false" is correct. Indeed, R then backtracks to u via port i, as specified in Case (a).

If v ∈ pred(u), then v = parent(u) iff for every neighbor w k connected to u by an edge with port number k ∈ {j -1, j -2, . . . , 0}, w k / ∈ pred(u). The robot does check this property in Case (b) of the description, by returning to u, and visiting all the w k 's while none of them is found in pred(u). Moreover, the robot ends the procedure just after returning to u by the edge j at u. Hence, Procedure Check Edge performs correctly in this case.

Finally, if v ∈ succ(u), then v = child(u) iff for every neighbor z l connected to v by an edge with port number l ∈ {i -1, i -2, . . . , 0}, z l / ∈ pred(v). In Case (c), the robot does check this property by visiting all these neighbors z l while none of them is found in pred(v). At this point, it remains for R to return to u (obviously, the port number leading from v to u cannot be stored in the robot's memory since it has only a constant number of states). Let k be the port number of the last edge incident to v that R visited before setting its variable edge to "false" or "child". We have 0 ≤ k ≤ i -1, z l / ∈ pred(v) for all l ∈ {k + 1, . . . , i -1}, and u ∈ pred(v). Thus u is identified as the first predecessor that is met when visiting all v's neighbors by successively traversing edges k + 1, k + 2, . . . of v. This is precisely what R does according to the description of the procedure in Case (c). Hence, Procedure Check Edge performs correctly in this case.

In summary, Procedure Check Edge performs correctly in all cases and so does the global exploration algorithm. It remains to compute the number of edge traversals performed by the robot during the exploration (including the calls to Check Edge).

We use again the same notations as in the description and in the proof of correctness of Procedure Check Edge. Let us consider the Procedure Check Edge(j) initiated at node u. Let v be other endpoint of the edge e with port number j at u, and let i be the port number of edge e at v. First observe that during the execution

• Reuven Cohen et al. j' j i i' i'' v u' u j'' v' u v v' u' i j i' i'' j' j''
(3) (1),(2) Case (a):. v ∈ sibling(u). Then edge e = {u, v} is traversed twice and no other edges are traversed during this execution of Procedure Check Edge.

Case (b):. v ∈ pred(u). Then R traverses only edges incident to u. Let k be the greatest port number of the edges leading to a node in pred(u) and satisfying k < j. If it does not exist, set k = 0. R explores twice each edge j, j -1, . . . , k + 1 of u, then twice edge k, and finally again twice edges k + 1, . . . , j -1, j. To summarize, edge k of u is explored twice, and edges k + 1, . . . , j -1, j of u are explored four times.

Case (c):. v ∈ succ(u). Then R traverses only edges incident to v. Let k be the greatest port number of the edges leading to a node in pred(v) and satisfying k < i. If it does not exist, set k = 0. R explores once edge j of u, twice each edge i -1, i -2, . . . , k + 1 of v, twice edge k, twice again edges k + 1, . . . , i -2, i -1, and finally once edge i of v (i.e., j of u). To summarize, edge i of u and edge k of v are explored twice and edges k + 1, . . . , i -2, i -1 of v are explored four times.

We bound now the number of times each edge e of the graph is traversed. Edge e = {u, v} is labeled i at u and j at v. Let us consider different cases (see Figure 1):

(1). e = {u, v} with v = parent(u). The edge e is in the spanning tree, and thus is explored twice outside any execution of the Procedure Check Edge. During Procedure Check Edge(j) at v, edge e is explored twice. e is also explored four times during Check Edge(i) at u, except if i = 0 where e is only explored twice during Check Edge(i) at u. If there exists an edge {u ′ , u} labeled i ′ at u and i ′′ at u ′ such that i ′ < i and u ′ ∈ pred(u), then edge e is explored twice during Procedure Check Edge(i ′ ) at u and twice again during Procedure Check Edge(i ′′ ) at u ′ . If there exists an edge {v ′ , v} labeled j ′ at v and j ′′ at v ′ such that j ′ < j and v ′ ∈ pred(v), then edge e is explored four times during Procedure Check Edge(j ′ ) at v and four times again during Procedure Check Edge(j ′′ ) at v ′ . To summarize, edge e is explored at most 20 times during a DFS.

(2). e = {u, v} with v ∈ pred(u) but v = parent(u). During Procedure Check Edge(j) at v, edge e is explored twice. e is also explored four times during Check Edge(i) at u. If there exists an edge {u ′ , u} labeled i ′ at u and i ′′ at u ′ such that i ′ < i

• 119 and u ′ ∈ pred(u), then edge e is explored twice during Procedure Check Edge(i ′ ) at u and twice again during Procedure Check Edge(i ′′ ) at u ′ . If there exists an edge {v ′ , v} labeled j ′ at v and j ′′ at v ′ such that j ′ < j and v ′ ∈ pred(v), then edge e is explored four times during Procedure Check Edge(j ′ ) at v and four times again during Procedure Check Edge(j ′′ ) at v ′ . To summarize, edge e is explored at most 18 times during a DFS.

(3). e = {u, v} with v ∈ sibling(u). During Procedure Check Edge(j) at v, edge e is explored twice. e is also explored twice during Check Edge(i) at u. If there exists an edge {u ′ , u} labeled i ′ at u and i ′′ at u ′ such that i ′ < i and u ′ ∈ pred(u), then edge e is explored four times during Procedure Check Edge(i ′ ) at u and four times again during Procedure Check Edge(i ′′ ) at u ′ . If there exists an edge {v ′ , v} labeled j ′ at v and j ′′ at v ′ such that j ′ < j and v ′ ∈ pred(v), then edge e is explored four times during Procedure Check Edge(j ′ ) at v and four times again during Procedure Check Edge(j ′′ ) at v ′ . To summarize, edge e is explored at most 20 times during a DFS.

Therefore, our exploration algorithm completes exploration in time at most 20m where m is the number of edges in the graph G.

Exploration while labeling

The above description assumes that the labeling of the graph was conducted by an external entity prior to the exploration process by the robot. As an alternative, we present here a minor change to the exploration algorithm, allowing the robot to color the graph while conducting the exploration process.

For simplicity, we assume that all nodes begin at an uncolored "blank" state, and that the robot can identify such blank nodes. Alternatively, one can assume that blank represents a forth color, making this a full 2-bit scheme. For the coloring process, the robot needs three extra bits of memory: a flag have colored and a 2-bit variable next color.

The exploration is performed in successive phases. The objective of phase i ≥ 0 is to color all nodes at distance i from r. More precisely, letting G i be the subgraph of the explored graph G induced by all nodes at distance at most i from the root r, the specification P (i) of phase i states that the robot starts phase i from the root, traverses all the edges of G i , colors all blank nodes by the color next color of the phase, and returns to the root.

At the beginning of the exploration (phase 0), the robot colors its current location white, sets next color to black, sets the flag have colored to false, and proceeds to phase 1.

For i ≥ 1, the robot's exploration in phase i is done as described in Subsection 2.1, with the restriction that procedure Check Edge is modified as follows. Assume Check Edge is called at node u for some edge e incident to u. The procedure proceeds the same as before, except that whenever the robot traverses an edge {x, y} from a colored node x to a blank node y, the following rules are applied.

-If the color of x is different from next color, then y is colored by next color, and the procedure carries on the same way as if y was already given the color next color when the robot entered it.

• Reuven Cohen et al.

-Otherwise (i.e., the color of x is next color), the robot returns to x and carries on just as if the edge {x, y} did not exist.

Whenever a node is colored next color, the flag have colored is set to true. For i ≥ 1, in order to switch from phase i to phase i + 1, the robot does the following. Whenever the exploration should have stopped in the original algorithm, the robot now checks if the flag have colored is set to true, and if so, clears it, sets next color ← succ(next color), and restarts the exploration (phase i + 1 starts). Otherwise, it stops.

Theorem 2.2. By the end of the execution of the modified algorithm, the graph is fully colored and the robot has explored the entire graph, terminating at the root.

Proof: We have to show that the algorithm meets its specification P (i) for every i ≥ 0. Define the layer i of G as the set of nodes at distance exactly i from r. For each i ≥ 0 and time t, we say that P roperty(i) holds at time t if the specification P (i) holds and the following holds at time t. 1) All nodes of G i are colored properly, i.e., according to the labeling L of the previous section, 2) Only nodes of G i are colored, 3) For i < D, next color is the color given by the labeling L to the nodes of layer i + 1.

We now prove that, at the end of phase i, P roperty(i) holds. At the end of phase 0, P roperty(0) holds by construction. For i ≥ 1, assume that at the end of phase i -1, P roperty(i -1) holds and let us prove that P roperty(i) holds at the end of phase i.

By the induction hypothesis, during phase i, all nodes of G i-1 are colored properly, i.e., according to the labeling L of the previous section.

Whenever the robot colors a node u during phase i, it has arrived from a node v that is colored and whose color is not next color. Therefore, v belongs to layer i -1, and u belongs to layer i. By the induction hypothesis, u is colored by the proper color next color.

By the modification of procedure Check Edge, whenever a non-colored node of layer i is visited by the robot coming from another node of layer i, the robot backtracks immediately. Therefore, every time the robot reaches a node u of layer i + 1, it comes from a colored node v of layer i. Since v is properly colored next color, u is not colored, and the robot backtracks, ignoring the edge {u, v}. Informally, this means that the behavior of the robot in G at phase i is the same as its behavior in the graph G i at the same phase i. In fact, there is only one difference, that occurs between siblings at layer i. In this situation, the modified procedure Check Edge backtracks and may ignore the edge. However, this has no impact on the exploration since anyway, even if all the nodes are colored a priori, the robot always backtracks when visiting a sibling.

By Theorem 2.1, during phase i, all the edges of G i are traversed, and at the end of the phase, the robot returns to the root. In fact, let T be the spanning tree of the explored graph G as induced by the labeling L of the previous section, and for i ≥ 0 let T i be the subtree of T spanning all nodes at distance at most i from the root r. The exploration proceeds as a DFS traversal of T i , thus all nodes of • 121 layer i are visited from a node of layer i -1, and hence are properly colored with next color. Hence specification P (i) holds.

When phase i is finished, next color is changed to succ(next color). Therefore, if i < D, at the end of phase i, the new next color is the color given by the labeling L to the nodes of layer i + 1.

Therefore, for each i ≥ 0, P roperty(i) holds at the end of phase i, and in particular, the specification P (i) holds. It follows that after D phases (where D is the diameter of the graph), the robot has completed coloring all nodes of the graph and has explored the entire graph. Nevertheless, another phase is performed, in which the robot discovers that the exploration and the coloring are actually completed.

A 1-BIT EXPLORATION-LABELING SCHEME FOR BOUNDED DEGREE GRAPHS

In this section, we describe an exploration labeling scheme using only 1-bit labels. This scheme requires a robot with O(log ∆) bits of memory for the exploration of graphs of maximum degree ∆. More precisely, we prove the following.

Theorem 3.1. For any integer ∆, there exists a robot with the property that for any graph G of degree bounded by ∆, it is possible to color the nodes of G with two colors (or alternatively, assign each node a 1-bit label) so that using the labeling, the robot can explore the graph G, starting from any given node and terminating after identifying that the entire graph has been traversed. The robot has O(log ∆) bits of memory, and the total number of edge traversals by the robot is O(∆ 10 m).

Note, that in the case where ∆ is constant, Theorem 3.1 implies that there exists a constant memory robot and a coloring with two colors of any graph G with maximum degree ∆, such that the robot can explore G using O(m) edge traversals.

To prove the theorem, we first describe a 1-bit labeling scheme L ′ for G = (V, E), i.e., a coloring of each node in black or white. Then, we show how to perform exploration using L ′ .

Labeling L ′ .. As for the labeling L of the previous section, pick an arbitrary node r ∈ V , called the root. Nodes at distance d from r are labeled as a function of d mod 8. Denote the distance between two nodes v and u in G by dist G (v, u). Partition the nodes into eight classes by letting

C i = {u ∈ V | dist G (r, u) mod 8 = i} for 0 ≤ i ≤ 7. Node u is colored white if u ∈ C 0 ∪ C 2 ∪ C 3 ∪ C 4 , and black otherwise. Let C1 = {u | dist G (r, u) = 1} C = {r} ∪ {u ∈ C 2 | N (u) = C1 }.
Lemma 3.2. There is a local search procedure enabling a robot of O(log ∆) bits of memory to decide whether a node u belongs to C and to C1 , and to identify the class C i of every node u / ∈ C.

Proof: Let B (resp., W) be the set of black (resp., white) nodes all of whose neighbors are also black (resp., white). One can easily check that the class C 1 and the classes C 3 , . . . , C 7 can be redefined as follows:

• Reuven Cohen et al.

-u ∈ C 6 ⇔ u ∈ B and there is a node in W at distance at most 3 from u; -u ∈ C 7 ⇔ u / ∈ C 6 , u has a neighbor in C 6 , and there is no node in W at distance at most 2 from u; -u ∈ C 1 ⇔ u is black, u has no neighbor in B, and u has a white neighbor v that has no neighbor in W.

-u ∈ C 5 ⇔ u is black, and u / ∈ C 1 ∪ C 6 ∪ C 7 ; -u ∈ C 3 ⇔ u ∈ W,
and there is a node in C 1 at distance at most 2 from u; -u ∈ C 4 ⇔ u has a neighbor in W, and there is no node in C 1 at distance at most 2 from u.

Based on the above characterizations, the classes C 1 and C 3 , . . . , C 7 can be easily identified by a robot of O(log ∆) bits, via performing a local search. For example, the characterization of C 6 is correct because of the following two observations. First, a node in B can only belong to C 6 or C 7 . Second, a node in C 7 never has a node in W at distance at most 3 from itself. The other characterizations can be proved similarly. Using the same ideas, the sets C1 and C can also be characterized as follows:

-u ∈ C1 ⇔ u ∈ C 1 and there is no node in C 7 at distance at most 2 from u; -u ∈ C ⇔ N (u) ⊆ C1 and every node v at distance at most 2 from u satisfies

|N (v) ∩ C1 | ≤ |N (u)|.
Using this we can deduce:

-u ∈ C 0 \ C ⇔ u / ∈ (∪ 7 i=3 C i ) ∪ C 1 and u has a neighbor in C 7 ; -u ∈ C 2 \ C ⇔ u / ∈ C ∪ C 1 , u has a neighbor in C 1 but no neighbor in C 7 .
It follows that a robot of O(log ∆) bits can identify the class of every node except for nodes in C.

Proof of Theorem 3.1:

The exploration algorithm for L ′ follows the same strategy as the exploration algorithm for L. Indeed, for u ∈ C i we have

pred(u) = N (u) ∩ C i-1 mod 8 , succ(u) = N (u) ∩ C i+1 mod 8 , sibling(u) = N (u) ∩ C i .
Therefore, due to Lemma 3.2, all instructions of the exploration algorithm using labeling L can be executed using labeling L ′ , but for the cases not captured in Lemma 3.2, i.e., C.

To solve the problem of identifying the root, we notice that each of the nodes in C can be used as a root and all the others can be considered as leaves in C 2 , without changing the classes of the nodes not belonging to C. Thus, when leaving the root, the robot memorizes the port p by which it should return to the root. When the robot leaves a node u ∈ C1 through port p, it leaves it in the up state and deletes the content of the variable storing p. Then, on the reached node v, the robot acts as if v would be in the class C 0 (which is the case since v is the root), i.e., it goes down through the next unexplored port, if there is one. When the robot • 123 leaves a node u ∈ C1 through a port different from p, and reaches a node in C, it leaves it in the down state and then acts as if the reached node would be in the class C 2 , i.e., it comes back to u in the up state.

If the exploration begins at the root, then the above is sufficient. To handle explorations beginning at an arbitrary node, it is necessary to identify the root. Since every node in C can be used as a root, it suffices to find one node of C by going up, and then start the exploration from it as described above.

It remains to compute the number of edge traversals performed by the robot during the exploration. The only edge traversals performed by the robot using L ′ but not performed by the robot using L are the edge traversals performed by the robot during the local search procedure enabling the robot to identify the class of the current node. Thus, the total number of edge traversals performed by the robot considered in this section is at most O(f (∆)m), where f (Delta) is the maximum number of edge traversals performed during the execution of the local search procedure.

The fact that f (Delta) = O(∆ 10 ) follows by observing that the local search procedure can be decided by inspecting the neighborhood of the node up to distance 10. Indeed, the membership of a node in sets C 6 , C 7 , C 1 , C 5 , C 3 , C 4 , C1 , C, C 0 \ C, and C 2 \ C can be decided by inspecting the neighborhood of this node up to distance, respectively, 4, 5, 3, 5, 5, 5, 7, 10, 6, and 10. We note that the bound on the total number of edge traversals can possibly be reduced further, using the following observation: once the robot has computed the class of the current node v using the described local search procedure, the class of any neighbor of v can only take three identified values. In this case, the robot can use a simplified procedure to identify the class of any subsequently visited node.

IMPOSSIBILITY RESULTS

In this section we aim to prove some bounds on exploration by robots with no memory, i.e., single state robots. We present two such bounds, one for exploring graphs with self loops (loops connecting a node to itself) and one for simple graphs, containing no self loops. We assume the robots are stateless and therefore the port traversed by the robot depends only on the color and the degree of the current node and of the label of the port by which the robot arrived at this node (unless the node is the starting node, in which case the port traversed depended only on the node's color and degree).

We aim to construct a graph (with self loops) that cannot be explored by a 1state robot. The constructed graph will be a star-like graph with the middle node having degree d, where some of its ports lead to degree one nodes while others loop back into the middle node. We will show that an adversary, that is given the details of the robot's transition table for each of c ≤ d/2 -1 colors, can construct such a graph which can not be explored by this robot. The proof relies on arguing that at least one node will not be explored for every possible coloring of the central node. We begin by several definitions that will help us construct such a graph.

Recall that when a 1-state robot enters a degree-d node v by port i, it will leave v by port j where j depends only on i, d and the color c of v. Thus for fixed d, each

• 125 V V 2 q p p 2 p p p p q 1 p p p o o r r k k-1 G and X G and X k-1 k 1 p 0 U U 0 Fig. 2.
In the right figure, the thick lines correspond the ports in X k-1 . Port p is the first port not in X k-1 that is visited by the robot at v, assuming that the starting node in u 0 and that v is colored with color c k . Port q is that port i h , where h is the smallest such that i h / ∈ X k-1 . In G k , Ports p and q (if they are different) are connected, constructing a loop, as depicted in the left figure

. X k then becomes X k = X k-1 ∪ {p, q}. t + r ≤ d/2 -1. Thus, t ≤ d/2 -1 and hence 2t + r + 1 ≤ d -1. Therefore, we have d -|X 0 | = d -(r + 1) > 2t.
Let k > 0, and let G k-1 and X k-1 be respectively a graph and a set satisfying the induction property for k -1. Assume first that v is colored by color c k and that the robot starts its traversal at u 0 . If the robot never visits vertices attached to v by ports not in X k-1 then the graph G k-1 and the set X k-1 satisfy P k . I.e., G k = G k-1 and X k = X k-1 . Otherwise, let p be the first port not in X k-1 that is visited by the robot at v, when starting at u 0 .

Define a sequence of ports (i l ) l≥1 as follows. Let i 1 be the port in X k-1 such that f k (i 1 ) = p. For all l ≥ 2, let i l be the port such that f k (i l ) = twin(i l-1 ). This sequence is well defined because f k is surjective. The sequence represents (in reverse order) the ports spanned by the robot on its exploration process towards port p.

Observe that there exists some l such that i l / ∈ X k-1 . Indeed, suppose, for the purpose of contradiction, that i l ∈ X k-1 for all l. Since X k-1 is finite, there exists some i l = i l+m for m ≥ 1. Let i l be the first port repeated twice in this process. If l > 1, then we have f k (i l ) = twin(i l-1 ) and f k (i l+m ) = twin(i l+m-1 ). Therefore twin(i l-1 ) = twin(i l+m-1 ), yielding i l-1 = i l+m-1 by bijectivity of f k , which contradicts the minimality of l. If l = 1, then we have i 1 = i 1+m , therefore i m = p, contradicting i j ∈ X k-1 for all j.

From the above, let h be the smallest index such that i

h / ∈ X k-1 . Let q = i h . If q = p, then set G k = G k-1 and X k = X k-1 ∪ {p}. If q = p
, then connect ports p and q to create a loop, denote the new graph G k and let X k = X k-1 ∪ {p, q}. See Figure 2.

In G k , if v is colored by color c k , then by the choice of p, starting at u 0 , the robot enters and exits v through ports in X k-1 until it eventually exits v through port p. After that, the robot goes back to v by port q. Port q was chosen so that it causes the robot to continue entering v on ports i h-1 , i h-2 , • • • i 1 , after which the robot exits v through port p, locking the robot in an infinite loop. Since the ports of v occurring in this cycle are all from X k , the robot does not visit any of the ports outside X k , as claimed. By induction, we have d

-|X k-1 | > 2(t -(k -1)). By the construction of X k from X k-1 , we have |X k | ≤ |X k-1 | + 2. Therefore d -|X k | > 2(t -k), which completes the correctness of G k and X k . If the color of v in G k is in {c 1 , • • • , c k-1
} then the robot is doomed to fail in exploring G k . Indeed, since starting at u 0 in G k-1 the robot does not traverse any of the vertices corresponding to ports not in X k-1 , then in G k too, the robot does not traverse any of the vertices corresponding to ports not in X k ⊇ X k-1 , and thus fails to explore G k because d -|X k | ≥ 1. This completes the proof of P k and thus the induction.

Theorem 4.2. For any d > 4, and for any 1-state robot using at most d/2 -1 colors, there exists a graph (with loops) with maximum degree d and at most d+1 vertices that cannot be explored by the robot.

Proof: Fix d > 4, and assume for contradiction that there exists a 1-state robot exploring all graphs of degree d colored with at most d/2 -1 colors. By Lemma 4.1, G t has property P t and thus at least one of its vertices is not explored by the robot if the node v is colored with a color in c 1 , c 2 , • • • , c t . If v is colored c t+i with 1 ≤ i ≤ r, then assume that the robot starts the traversal at vertex u 0 . Since the edge labeled p i leads to a degree-1 vertex in G t , this vertex will never be visited by the robot, by definition of p i . Therefore the graph G t cannot be explored by the robot.

The theorem above makes use of graphs with loops. For graphs without loops we use the same construction, replacing loops with simple subgraphs without loops. However, in a loop, a robot entering the loop through one port will immediately return to its last visited node through the other port. If the loop is replaced by a more complex structure we need to guarantee that the robot will necessarily return to the node from which it entered this structure using the second port connected to this structure.

Consider a node w of degree d, accessible from the rest of the graph through two ports, p and q, and all its other d -2 ports lead to leaves. We aim to show that there exists a labeling of the two ports, such that entering the node through one of them, will guarantee leaving through the other, regardless of the color used for the node. As before we define the set {p 1 , • • • , p r } of ports excluded from non-surjective colors and have each of them lead to a leaf. We also note, that by looking at each function f i as a permutation on d elements, if for some f i , the cycle decomposition of this permutation consists of more than two cycles, then w cannot be colored by f i because whatever ports p and q are chosen, the robot can visit only ports corresponding to the cycles that p and q belong to. Therefore we may assume that the cycle decomposition of each of the relevant f i consists of at most two cycles. We will term such a color (whose function is surjective and contains at most two cycles) as useful.

Using the next two lemmas we show that for high enough degree d, we can always choose two ports p, q / ∈ {p 1 , • • • , p r } such that for every useful color they belong to the same cycle. must leave through q and vice versa. It follows that whenever the robot enters G L from v in port i it must return to v in port j (and vice versa). Therefore, the loop L in the proof of Theorem 4.2 can be replaced by G L .

DISCUSSION

It was known that there is no 0-bit exploration-labeling scheme, even for bounded degree graphs. We proved that there is a 2-bit exploration-labeling scheme for arbitrary graphs, and that there is a 1-bit exploration-labeling scheme for bounded degree graphs. It remains open whether or not there exists a 1-bit explorationlabeling scheme for arbitrary graphs.

Fig. 1 .

 1 Fig. 1. Notations for case (1), (2) and (3) of the analysis of the Procedure Check Edge only edges incident to u and v are traversed. More precisely:

Fig. 3 .

 3 Fig.3. The loop L (with ports i and j) in the right figure, is replaced by the subgraph G L , as depicted in the left figure. Ports p and q are chosen such that {p, q} ∩ {p 1 , p 2 , • • • pr} = ∅ and such that they belong to the same cycle, for every useful color. It follows that if the robot exits v through port i, it must return to v via port j, and vice versa.

•

  Reuven Cohen et al.

•

  Reuven Cohen et al.

ACM Journal Name, Vol. V, No. N, Month 20YY, Pages 111-0??.

ACM Journal Name, Vol. V, No. N, Month 20YY.

Supported by the project "PairAPair" of the ACI Masses de Données, the project "Fragile" of the ACI Sécurité et Informatique, and by the project "Grand Large" of INRIA. grant from the Israel Science Foundation.

• Reuven Cohen et al.

color corresponds to a mapping from entry ports to exit ports, namely, a function from {0, 1, • • • , d -1} to {0, 1, • • • , d -1}. Partition the functions corresponding to the colors of nodes of degree d into surjective functions f 1 , f 2 , • • • , f t and nonsurjective functions g 1 , g 2 , • • • , g r . We have 0 < t + r ≤ d/2 -1. Let c i be the color corresponding to f i , and c t+i be the color corresponding to g i . For each g i , choose p i to be some port number not in the range of g i . Since for each i, p i is not in the range of g i , starting from a node colored by c t+i the robot will never traverse port p i .

To show that the central node can not be colored by any of the colors c i , 1 ≤ i ≤ t (the colors with a surjective transition function) a graph should be constructed in which coloring the central node by any of these colors will result in at least one of the leaves not being explored. To do that we construct a family

(1) G k has exactly one degree-d vertex v (possibly with loops);

(2) all edges are either loops incident to v, or edges leading from v to some degree-1 node;

(3) edges labeled p 1 , p 2 , • • • , p r at v (if any, i.e., if r > 0) are not loops (and thus lead to degree-1 nodes); (4) the edge labeled p 0 leads to some distinguished degree-1 node, denoted by u 0 ;

(5) there exists a set

, and for which, in G k , edges with port number not in X k lead to degree-1 vertices.

For a given graph G k-1 , we define the following: For a port i ∈ {0, 1, • • • , d -1}, set twin(i) = j if there exists a port j and a loop labeled by i and j in G k-1 ; Set twin(i) = i otherwise. This definition of twin corresponds to the port by which the robot reenters the central node after leaving it using port i; if port i leads to a leaf then the robot returns from the leaf to the central node using the same port, and if port i leads to a loop returning through port j, the robot immediately reenters the central node through port j.

We prove the following property for any k = 0, • • • , t:

More precisely any vertex attached to v by a port ∈ X k is not visited by the robot.

The proof relies on starting with a star graph, and for each color, k, replacing two nodes by a loop (if needed). The loop is formed between appropriate ports, chosen such that the robot will return to previously visited ports without completing the exploration of all ports.

Lemma 4.1. For every k = 0, . . . , t there exists a graph G k , having property P k .

Proof: We prove the lemma by induction on k. First, note that Property P 0 is trivially true for every graph. Still, to ease the induction proof, we would like to define the graph G 0 and the set X 0 . Let G 0 be the star composed of one degree-d vertex v and d leaf vertices. Let Proof: We prove by induction on k. For k = 1, f 1 contains at most two cycles permuting the d ports, therefore one of these cycles contains at least d/2 ports.

Assume that the induction hypothesis is true for k = n, i.e., there are s ≥ d/2 n ports that are in the same cycle for each of f 1 , • • • , f n . Now, f n+1 contains at most two cycles, so one of them contains at least half of the s ports. Therefore, there are at least s/2 ≥ d/2 n+1 ports that belong to one cycle in each of the n + 1 functions, completing the induction.

Lemma 4.4. For any d > 4 and for c ≤ ⌊log d⌋ -2 colors, there exists at least two ports p, q ∈ {0, 1,

that belong to the same cycle for all useful colors.

Proof: Assume that there are k ≤ t useful colors, by Lemma 4.3 there are at least d/2 k ports belonging to the same cycle for all useful colors. Now d/2 k ≥ d/2 t ≥ 2 2+c-t = 2 2+r = 4 • 2 r . Therefore, there are at least 4 • 2 r ports belonging to one cycle for all useful colors, and 4 • 2 r ≥ 2 + r for all r ≥ 0. Thus, p and q can always be selected to be other than p 1 , p 2 , • • • , p r .

We now turn to the main theorem, building on the construction with loops of Theorem 4.2 presented above, and replacing the loops by paths in the graph.

Theorem 4.5. For any d > 4 and for any 1-state robot using at most ⌊log d⌋ -2 colors, there exists a graph of maximum degree d, without loops, that cannot be explored by the robot.

Proof: As in the proof of Theorem 4.2, denote the functions corresponding to the colors by f 1 , f 2 , • • • , f t , g 1 , g 2 , • • • , g r where the f i 's are surjective functions and the g i 's are non-surjective ones. For each g i , choose p i to be some port number not in the range of g i . We use the same proof as for Theorem 4.2, except that we replace each loop L of the construction in there by a loopless graph. For a loop L of vertex v, with port numbers i and j, let G L be the following graph. (See Figure 3.) Connect v by edges to two new vertices w and w ′ , add the edge (w, w ′ ), and connect w (respectively, w

). We now set the port numbering for G L . Assign the port numbers i and j for the edges (v, w) and (v, w ′ ). At w (respectively, w ′ ) use the port numbers p 1 , p 2 , • • • , p r for the edges (w, n 1 ), (w, n

). The port numbers p and q that w uses for the edges (w, v) and (w, w ′ ) are the same as the port numbers that w ′ uses for the edges (w ′ , v) and (w ′ , w). They are chosen to be in the same cycle for all useful colors, as shown in Lemma 4.4.

We immediately get that w and w ′ cannot be colored by a color whose corresponding function is in the set g 1 , g 2 , • • • , g r since these functions are not surjective and ports {p 1 , p 2 , • • • , p r } lead to leaves of w and w ′ . Also, w and w ′ cannot be colored by a non-useful color, since it contains at least three cycles, and since w and w ′ can only be entered through two ports (p and q) all ports belonging to cycles not containing p and q will not be visited.

Therefore, w and w ′ must be colored by a useful color. However, for all useful colors, p and q belong to the same cycle, and thus a tour entering through port p


Mnacho Echenim

Radu Iosif

Nicolas Peltier

Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules

Keywords: Separation Logic, Inductive Definition, Decidability

 if the inductive rules satisfy three conditions, namely progress, connectivity and establishment. We show that entailment is undecidable if the latter condition is dropped, thus drawing a much clearer frontier for (un)decidability.

Introduction

Separation Logic (SL) is widely used in program verification to reason about programs manipulating dynamically allocated data structures [np]modif [START_REF] Ishtiaq | Bi as an assertion language for mutable data structures[END_REF]. SL formulae describe heaps, i.e. finite partial functions mapping locations (memory addresses) to tuples of locations (records) of a fixed size. [np]modif A location is allocated if it occurs in the domain of the considered heap. A formula x → (y 1 , . . . , y κ ) states that the image of the location associated with x in the heap is the tuple of locations associated with (y 1 , . . . , y κ ), whereas φ 1 * φ 2 states that the heap can be split into two disjoint parts satisfying φ 1 and φ 2 , respectively. Describing unbounded data structures (lists, trees, etc.) is possible by the use of predicate symbols, the interpretation of which is given by a set of user-defined inductive rules. These SL formulae, in which boolean conjunction does not occur and negation is restricted to disequalities, are commonly called symbolic heaps. Testing entailment between symbolic heaps is known to be decidable for a class of inductive definitions satisfying three natural conditions [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF]: [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF] progress, stating that every inductive rule allocates exactly one memory cell, (2) connectivity, ensuring that the locations allocated during the unfolding of a predicate form a tree-like connected structure and (3) establishment, stating that every existentially quantified variable introduced during the unfolding of inductive predicates must be eventually allocated (in the sense that it must be asserted equal to a variable y such that an atom y → (. . . ) occurs in the unfolding). These conditions play very different rôles. Condition (1) is actually not restrictive and is considered for simplicity only. In contrast, Condition (2) is crucial for decidability: entailments are undecidable for inductive definitions that are not connected, because then the inductive definitions may be used to encode context-free languages, the inclusion of which is known to be undecidable. The remaining question is whether condition (3) is actually required for decidability or whether it can be ignored. We show that discarding this condition leads to undecidability. The precise rôle of establishment for decidability of entailments between symbolic heaps has been an open problem since establishment was identified as a condition ensuring, with progress and connectivity, decidability of entailments between symbolic heaps [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF]. The proof of [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF] used a reduction of the entailment between symbolic heaps to the (decidable) satisfiability of monadic second order logic on graphs with bounded treewidth [START_REF] Courcelle | The monadic second-order logic of graphs. I. Recognizable sets of finite graphs[END_REF] and establishment was crucial to ensure that the considered heaps have a bounded treewidth. Later, a doubly exponential decision algorithm was designed [START_REF] Pagel | Beyond symbolic heaps: Deciding separation logic with inductive definitions[END_REF], and we recently showed that establishment can be replaced by a strictly more general condition restricting the form of the disequations in the system [START_REF] Echenim | Decidable entailments in separation logic with inductive definitions: Beyond establishment[END_REF]. The undecidability proof for non-established definitions given here implies the undecidability of entailments for definitions that cannot be transformed into the restricted disequations form [START_REF] Echenim | Decidable entailments in separation logic with inductive definitions: Beyond establishment[END_REF].

Separation Logic

Let κ ≥ 0 be a natural number, V and C be two disjoint sets of symbols (denoting respectively variables and constants 1 , and P be a set of predicate symbols. Each symbol p ∈ P is associated with a unique arity #(p) ≥ 1. The set of separation logic symbolic heaps φ is inductively defined as follows, where

x, x , y 1 , . . . , y κ , z 1 , . . . , z #(p) ∈ V ∪ C , u ∈ V and p ∈ P :

φ ::= x ≈ x | x ≈ x | x → (y 1 , . . . , y κ ) | φ * φ | p(z 1 , . . . , z #(p) ) | ∃u . φ.
1 Constants are introduced only to improve readability. One could replace them by variables added as parameters to every predicate symbol, and adding disequality constraints x ≈ y for all x, y ∈ C , stating that all constants are mapped to distinct locations. Hence the undecidability result holds also for C = / 0.

2

A formula is predicate-free if it contains no symbols from P . We denote by var(φ) the set of variables freely occurring in φ. A substitution is a partial mapping from V to V ∪ C . The substitution of domain {x 1 , . . . , x n } mapping every variable

x i to t i is denoted by [x i ← t i | 1 ≤ i ≤ n].
For every formula φ and substitution σ, φσ denotes the formula obtained by replacing each free occurrence of a variable x in φ by σ(x) (bound variables are renamed to avoid collisions).

Let U be a countably infinite set of locations, with C ⊆ U. A structure is a pair (s, h) where s is a store, i.e., a total mapping from V ∪ C to U that is the identity on C ; and h is a heap, i.e., a partial finite mapping from U to U κ . Two heaps h 1 and h 2 are disjoint iff dom(h 1 ) ∩ dom(h 2 ) = / 0, and h 1 h 2 denotes the union of disjoint heaps.

A system of inductive definitions (SID) R is a set of rules p(x 1 , . . . , x #(p) ) ⇐ φ, where x 1 , . . . , x #(p) are pairwise distinct variables and φ is a symbolic heap

with var(φ) ⊆ {x 1 , . . . , x #(p) }. A system R is progressing and connected if ev- ery rule in R is of the form p(x 1 , . . . , x #(p) ) ⇐ ∃y 1 , . . . , y n . x 1 → (u 1 , . . . , u #(p) ) * * m i=1 p i (y i 1 , . . . , y i #(p i ) )
, where for all i ∈ 1, m , we have

y i 1 ∈ {u 1 , . . . , u #(p) }. For any formula φ, we write φ → R ψ if ψ is obtained from φ by replacing an occurrence of a predicate atom p(x 1 , . . . , x #(p) ) by ρ[y i ← x i | 1 ≤ i ≤ #(p)],
where R contains a rule p(y 1 , . . . , y #(p) ) ⇐ ρ and the existential variables of ρ are α-renamed to avoid collisions. As usual, → * R denotes the reflexive and transitive closure of → R . A formula ψ such that φ → * R ψ is called an R -unfolding of φ. A SID R is established if, in every predicate-free R -unfolding ψ of a predicate atom p(x 1 , . . . , x #(p) ), each existentially quantified variable in ψ is asserted equal to a variable x, where x → (y 1 , . . . , y κ ) is a an atom of ψ.

For all structures (s, h), symbolic heaps φ containing no predicate atom and SIDs R , we write (s, h) |= φ iff one of the following holds: (i) φ ≡ x ≈ x (resp.

φ ≡ x ≈ x ), dom(h) = / 0 and s(x) = s(x ) (resp. s(x) = s(x )); (ii) φ ≡ x → (y 1 , . . . , y κ ), dom(h) = {s(x)} and h(s(x)) = (s(y 1 ), . . . , s(y κ )); (iii) φ ≡ φ 1 * φ 2 and h = h 1 h 2 where (s, h i ) |= φ i ,
for all i ∈ {1, 2}; (iv) φ ≡ ∃x . φ and there exists a store s coinciding with s on all variables and constants distinct from x such that (s , h) |= φ . This definition is extended to formulae containing predicate symbols as follows:

(s, h) |= R φ iff (s, h) |= R ψ, for some predicate-free R -unfolding ψ of φ.
[np]modifs Note that (dis)equations are satisfied only in empty heaps. This slightly departs from usual definitions [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF][START_REF] Ishtiaq | Bi as an assertion language for mutable data structures[END_REF] but simplifies notations by getting rid of standard conjunctions.

Encoding the Post Correspondence Problem

The undecidability proof uses a reduction from a variant of Post's Correspondence Problem (PCP). We denote by w[i] the i-th character of the word w, and by |w| its length, so that w = (w[1], . . . , w[|w|]). We recall that the PCP asks, given two sequences u i = (u i 1 , . . . , u i N ) (with i = 1, 2) of words on the same alphabet V, whether there exists a nonempty sequence s = (s 1 , . . . , s G ) of elements of 1, N (called a solution of the PCP) such that u1

s 1 . . . . .u 1 s G = u 2 s 1 . . . . .u 2 s G .
The latter word is called a witness of the PCP and its length Σ G g=1 |u i g | will be denoted by L. PCP is a well-known undecidable problem. We assume that all the words in u i are nonempty (which does not impact the undecidability proof of the PCP). We consider a slightly adapted version of the PCP, in which: (i) The last element of both sequences of words is a special character $ = u 1 N = u 2 N , not occurring in the words u i n , for i ∈ {1, 2}, n ∈ 1, N -1 ; and (ii) any solution must be such that

G > 1, s G = N and s g = N if g < G.
It is clear that the standard PCP can be reduced to the adapted version, which is thus also undecidable. We denote by M i the maximal length of the words in u i , i.e.

M i def = max{|u i n | | n ∈ 1, N }, for i ∈ {1, 2} and let M def = max({M 1 , M 2 }).
We consider two special constants nil and ⊥, and we associate all natural numbers m ∈ 1, M and all elements a ∈ V with pairwise distinct constants also distinct from nil and ⊥. These constants will be, for the sake of readability, also denoted by m or a (assuming, w.l.o.g., that V ∪ N ∪ {⊥, nil} ⊆ C and V ∩ N = / 0). We assume next that κ = 6, i.e. we fix the number of record fields. The encoding could easily be adapted for any κ ≥ 2, using binary trees to represent tuples of elements, but this would greatly hinder readability, because of the progress condition which requires that every rule allocates exactly one location. For readability, we shall actually consider elements referring to tuples of any length n ≤ 6, where missing elements are implicitly replaced by the constant ⊥. Hence the notation x → (y 1 , . . . , y n ) for n ≤ 6 stands for x → (y 1 , . . . , y n , ⊥ 6-n ). For the sake of conciseness, we allow disjunctions in the right-hand side of the inductive rules: a rule p( x) ⇐ φ * (ψ 1 ∨ ψ 2 ) stands for {p( x) ⇐ φ * ψ 1 , p( x) ⇐ φ * ψ 2 }. We first show that the solutions of the PCP can be encoded by structures of a specific form. Definition 1. A heap h is a PCP-encoding if there exists a word w with L def = |w| > 1, a natural number G > 1 and pairwise distinct locations 1 , . . . , L+1 and 2. For every l ∈ 1, L , h( l ) is of the form ( l+1 , w[l], 1 l , p 1 l , 2 l , p 2 l ), for locations 1 l , 2 l and integers p 1 l , p 2 l ∈ 1, M , with

1 1 = 2 1 = 1 , 1 L = 2 L = G and p 1 1 = p 2 1 = p 1 L = p 2 L = 1. 3.
For every g ∈ 1, G , h( g ) is of the form ( g+1 , s g ) for some s g ∈ 1, N , with s G = N and s g = N if g < G. The location 1 is called the root of h. We denote w(h) def = w and s(h) def = (s 1 , . . . , s G ); clearly h uniquely defines w(h) and s(h).

nil s 1 s 2 N w[1] w[2] w[L] 1 l 1 l 2 l p 1 l p 2 l • • • • • • • • • • • • • • • 1 1 L K Figure 1:
Encoding of a PCP Solution by a Heap

[np]capital h, for consistency in titles ?

The sequence 1 , . . . , L encodes the sequence of characters w[1],. . . , w[L] in a witness w. Each location l refers to a tuple containing the next element of the sequence l+1 as well as the character w[l], and locations 1 l , p 1 l , 2 l , p 2 l , which will be used to denote the position of the character within the words u 1 s 1 . . . . .u 1 s G and u 2 s 1 . . . . .u 2 s G (see Def. 2). The sequence 1 , . . . , G represents the solution s. Each location g points to a tuple containing the next element of the sequence g+1 and the g-th component of s (see Fig. 1). Definition 2. A PCP-encoding h is i-consistent for i = 1, 2 if, for all l ∈ 1, L , there exists g ∈ 1, G such that, with the notations of Def. 1, i l = g and: 1. w[l] is the p i l -th character of the word u i s g (i.e., w[l] = u i s g [p i l ]). 2. If l = L and p i l < |u i s g | then i l+1 = g and p i l+1 = p i l + 1. 3. If l = L and p i l = |u i s g | then g < G, i l+1 = g+1 and p i l+1 = 1.

Lemma 3. A PCP admits a solution iff there exists a PCP-encoding that is both 1-consistent and 2-consistent.

Proof. Assume that the PCP admits a solution s of length G, with witness w and let L = |w|. We construct a PCP-encoding as follows. Let 1 , . . . , L , 1 , . . . , G be pairwise distinct locations distinct from all constants. Let L+1 def = G +1 def = nil, and let h be a heap of domain { 1 , . . . , L , 1 , . . . , G }, such that: (i) For every

l ∈ 1, L , h( l ) def = ( l+1 , w[l], g 1 l , p 1 l , g 2 l , p 2 l )
, where g i l is the greatest element in 1, G with |u i s 1 . . . . .u i

s g i l -1 | < l, and p i l def = l -|u i s 1 . . . . .u i s g i l -1 |. (ii) For every g ∈ 1, G , h( g ) def = ( g+1 , s g ).
It is straightforward to check that h is a PCPencoding. Conversely, let h be a PCP-encoding that is i-consistent for all i = 1, 2, and let w def = w(h) and s def = s(h). By induction on l, we can show, by a case analysis on whether p i l < |u i

s g i l |
or not, and using Conditions 2 and 3 of Def.

2 that [np]change here, because there was a latex pb with command either for every i ∈ {1, 2} and l ∈ 1, L , the following equality holds:

w[1]. . . . .w[l] = u i s 1 . . . . .u i s g i l -1 .u i s g i l [1]. . . . .u i s g i l [p i l ] (1)
.

I(x) ⇐ ∃x , y, z . x → (x , a, y, 1, y, 1) * W (x , z) * S(y, z) (2)
W (x, z) ⇐ ∃x , y 1 , y 2 . x → (x , a, y 1 , p 1 , y 2 , p 2 ) * W (x , z) (3) W (x, z) ⇐ x → (nil, $, z, 1, z, 1) (4)
S(y, z) ⇐ ∃y . y → (y , n) * S(y , z) if n < N (5) S(y, z) ⇐ y → (nil, N) * y ≈ z (6) A(x) ⇐ ∃x , a, z 1 , p 1 , z 2 , p 2 . x → (x , a, z 1 , p 1 , z 2 , p 2 ) * A(x ) (7) A(x) ⇐ ∃x , a, z 1 , p 1 , z 2 , p 2 . x → (x , a, z 1 , p 1 , z 2 , p 2 ) (8) C(x, x , a, z 1 , p 1 , z 2 , p 2 ) ⇐ x → (x , a, z 1 , p 1 , z 2 , p 2 ) * A(x ) (9) C(x, x , a, z 1 , p 1 , z 2 , p 2 ) ⇐ x → (x , a, z 1 , p 1 , z 2 , p 2 ) (10)
B(x) ⇐ ∃x , a, y . x → (x , a, y, 1, y, 1) * B(x

) * A(y) (11) B(x) ⇐ ∃x , a, z 1 , p 1 , z 2 , p 2 . x → (x , a, z 1 , p 1 , z 2 , p 2 ) * B(x ) (12) B(x) ⇐ ∃x , a, z 1 , z 2 , p 2 , z 1 . x → (x , a, z 1 , p 1 , z 2 , p 2 ) * A(x ) * C(z 1 , z 1 , n, ⊥, ⊥, ⊥, ⊥) * a ≈ u 1 n [p 1 ] if p 1 ≤ |u 1 n | (13) B(x) ⇐ ∃x , a, z 1 , z 2 , p 2 , a , z 1 , p 1 , z 2 , p 2 , z 1 . x → (x , a, z 1 , p 1 , z 2 , p 2 ) * C(x , a , z 1 , p 1 , z 2 , p 2 ) * C(z 1 , z 1 , n, ⊥, ⊥, ⊥, ⊥) * (z 1 ≈ z 1 ∨ p 1 ≈ p 1 + 1) if p 1 < |u 1 n | (14) B(x) ⇐ ∃x , a, z 1 , z 2 , p 1 , p 2 , a , z 1 , z 2 , p 2 , z 1 . x → (x , a, z 1 , p 1 , z 2 , p 2 ) * C(x , a , z 1 , p 1 , z 2 , p 2 ) * C(z 1 , z 1 , n, ⊥, ⊥, ⊥, ⊥) * (p 1 ≈ 1 ∨ z 1 ≈ z 1 ) if p 1 = |u 1 n | (15) Figure 2: The SID R π for the PCP Instance π = (u 1 , u 2 ) (for all a ∈ V, p 1 , p 2 ∈ 1, M , n ∈ 1, N )
Let π = (u 1 , u 2 ) be an instance of PCP, where u i = (u i 1 , . . . , u i N ), i = 1, 2. We show how to transform i-consistent PCP-encodings into SL formulae. Let R π be the set of rules in Fig. 2. We show that I defines the PCP-encodings of π (Def. 1).

[np]modifs Intuitively W and S allocate the locations 1 , . . . , L+1 and 1 , . . . , G+1 respectively. The existential variables y 1 , y 2 in (3) are not allocated (the corresponding pointers w [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF], w [START_REF] Ishtiaq | Bi as an assertion language for mutable data structures[END_REF], . . . in Fig. 1 are pending), hence this rule is not established.

Lemma 4. (s, h) |= R π I(x 1 ) iff h is a PCP-encoding of root s(x 1 ). Proof. (s, h) |= R π I(x 1 ) iff (s, h) |= φ for some predicate-free formula φ with I(x 1 ) → * R π φ. By Rule (2), I(x 1 ) → * R π φ iff there exists a 1 ∈ V s.t. ∃x 2 , y 1 , z. x 1 → (x 2 , a 1 , y 1 , 1, y 1 , 1) * W (x 2 , z) * S(y 1 , z) → * R π φ. Any → R π -derivation from W (x 2 , z)
starts by a sequence of application of Rule (3) followed by one application of (4).

Thus I(x 1 ) → * R π φ iff there exists L ∈ N, a 1 , . . . , a L-1 ∈ V, p 1 2 , p 2 2 , . . . , p 1 L-1 , p 2 L-1 ∈ 1, M s.t. ∃x 2 , . . . , x L , y 1 , z. x 1 → (x 2 , a 1 , y 1 , 1, y 1 , 1) * ψ * S(y 1 , z) → * R π φ, where ψ def = * L-1 l=2 x l → (x l+1 , a l , y 1 l , p 1 l , y 2 l , p 2 l ) * x L → (nil, $, z, 1, z, 1
). Applying Rule (5) G -1 times and then Rule (6), we deduce that I(x 1 ) → * R π φ iff there exists

L ∈ N, G ∈ N, a 1 , . . . , a L-1 ∈ V, p 1 2 , p 2 2 , . . . , p 1 L-1 , p 2 L-1 ∈ 1, M , n 1 , . . . , n G-1 ∈ 1, N -1 s.t. ∃x 2 , . . . , x L , y 1 , . . . , y G . x 1 → (y, a 1 , y 1 , 1, y 1 , 1) * ψ * ψ → * R φ where ψ def = * G-1 g=1 y g → (y g+1 , n g ) * y G → (nil, N) * y G ≈ z.
Using this equivalence, it is easy to check that (s, h) |= I(x 1 ) iff h is a PCP-encoding with root s(x 1 ).

Predicate B defines the PCP-encodings that are not i-consistent, for some i = 1, 2 (Def. 2). Such structures necessarily contain locations l and g contradicting one of Cond. 1, 2 or 3 from Def. 2. Rule (11) is applied when g is such that g > 1. It allocates the first element 1 of the witness, then invokes A(y) to allocate all elements 1 , . . . , g-1 , and the predicate B(x ) to allocate the remaining elements. Note that, [np]modifs thanks to the rules (7) and (8), A allocates arbitrary linked structures, with the link on the first record field (all the pointers in the list are pending and the resulting list does not necessarily end with nil). Predicate C is similar to A, but has 6 additional parameters denoting the heap image of the first allocated location. Rule (12) is applied l -2 times to allocate locations 2 , . . . , l-1 and also to allocate 1 in the case where g = 1 (this case is considered apart since the sequence 1 , . . . , g-1 is empty). The remaining rules allocate the faulty location l . Rules (13-15) handle the case where the heap is not 1-consistent. Rule (13) allocates a location contradicting Cond. 1 in Def. 2. The predicates A(y) and C(z 1 , y , n, ⊥, ⊥, ⊥, ⊥) are used to allocate locations l+1 , . . . , L , and g , . . . , G , respectively. Similarly, Rules (14) and (15) allocate a location contradicting Cond. 2 or 3 in Def. 2, respectively. The rules corresponding to the case where the heap is 2-consistent are defined in a similar way (they are omitted for conciseness).

, . . . , G+1 with L+1 = G+1 = nil, such that: 1. dom(h) = { 1 , . . . , L , 1 , . . . , G }.

Lemma 5. Let h be a PCP-encoding and let s be a store such that s(x) is the root of h. The following equivalence statement holds: (s, h) |= R B(x) iff h is not i-consistent, for some i = 1, 2.

Proof. We use the same notations as in Def. 1. ⇒ ⇒ ⇒: Assume that (s, h) |= R π B(x). Then there exists a predicate-free unfolding φ of B(x) such that (s, h) |= R π φ. By definition of the rules defining B, this entails that one of rules (13), ( 14) or (15) (or the corresponding rules for i = 2) must have been applied at some point in the derivation, since these are the only rules that can eliminate the predicate. By symmetry we assume that one of the rules corresponding to i = 1 is applied. If Rule (13) is applied, then there exist locations l, l , l , l 1 and l 2 such that h

Since h is a PCP-encoding, this is possible only if l = l , for some l ∈ 1, L and l 1 = g , for some g ∈ 1, G . Then h falsifies Cond. 1 of Def. 2, hence h is not 1-consistent. If Rule (14) is applied then there exist locations l, l , l , l 1 , l 2 , l 1 , l 2 and l 1 such that

Since h is a PCP-encoding, we must have l = l and l = l+1 for some l ∈ 1, L , and l 1 = g , for some g ∈ 1, G . Therefore, Cond. 2 of Def. 2 is falsified. The proof is similar if Rule (15) is applied: we have p 1 = |u 1 n |, and either l 1 ≈ l 1 or p 1 = 1, which entails that Cond. 3 of Def. 2 is falsified.

⇐ ⇐ ⇐: Assume that h is not i-consistent, for some i = 1, 2. We assume that i = 1, the proof for i = 2 is symmetric. By definition of a PCP-encoding, there exists a store s such that s(x) = s (x) and:

where x l , y i l , y g ∈ V , a l ∈ V, p i l ∈ 1, M and n g ∈ 1, N , for all l ∈ 1, L , g ∈ 1, G and i ∈ {1, 2}. The location s(x 1 ) is the root of the heap, thus we have s(x) = s(x 1 ), and we may assume, w.l.o.g., that x = x 1 . Since by hypothesis h is not 1-consistent, there exist l ∈ 1, L and g ∈ 1, G such that one of the conditions in Def. 2 is falsified. Observe that, according to Def. 2, this entails that s(y 1 l ) = s(y g ). We also have l < L; indeed, it is easy to check that the faulty location cannot be the last one, since, by definition of a PCP-encoding, this location is associated with the special character $ and index n G = N, with u i N = $ and p i L = 1. We therefore have:

, where:

2 ) ( †), using Rule (9) if l < L -1 and Rule (10) otherwise. Similarly, ψ 2 |= R π A(y g+1 ) and

l ], hence, by Rule (13), using ( ) and ( ‡), we get that x l → (x l+1 , a l , y l 1 , p l 1 , y l 2 , p l 2 ) * φ 2 * y g → (y g+1 , n g ) * ψ 2 |= R π B(x l ). If Cond. 2 or 3 are falsified, then we get the same result, using the rules ( 14) and (15), instead of (13), and Relation ( †) instead of ( ). If g = 1, then, by applying Rule (12) g -1 times, we deduce that (s, h) |= R π B(x 1 ). If g > 1, then we get the same result by applying Rule (11) once and Rule (12) g -1 times, using the fact that ψ 1 |= R π A(y g ).

Putting everything together, we get the stated result: Theorem 6. The entailment problem is undecidable for systems of inductive definitions satisfying the progress and connectivity condition, but not the establishment condition.

Proof. Consider an instance π of the (adapted) PCP. By Lemma 3, the PCP has a solution iff there exists a PCP-encoding that is i-consistent, for i = 1, 2. By Lemmas 4 and 5, we can compute a system of inductive rules R π such that h is a PCP-encoding iff (s, h) |= R π I(x 1 ), and h is i-consistent for all i = 1, 2 iff (s, h) |= R π B(x 1 ); i.e., such that the PCP has a solution iff I(x 1 ) |= R π B(x 1 ). It is easy to check that R π is progressing and connected but not established, see for instance Rules (3), (7), (8) and (12) in Fig. 2. Since the PCP is undecidable, the proof is completed.


The Enigma of Reason opens up with a double enigma. Many scholars throughout history have thought of reason as a cognitive silver bullet, which would allow humans to innovate, to overcome their cognitive and emotional failings, to solve a wide variety of problems, and to better understand the world around them. The first enigma, then, is why only humans would be endowed with such a superpower? Why wouldn't such a capacity, with its multiple advantages, have evolved in many other organisms? The second enigma stems from the mismatch between this lofty view of reason, and reality: experience and experiments have shown time and again that human reason is as flawed, biased, and prone to mistakes as the rest of our cognition.

We offer a twofold answer to these two enigmas. First, we develop a new understanding of what reason is, and new hypotheses about what reason is for (Parts II and III). Second, we defend these hypotheses, focusing on the functional hypotheses developed in Part III (Parts IV and V).

Part I, "Shaking Dogma," offers a brief critical look at state of the art in the study of human reason. Since its inception in the 1960s, the psychology of reasoning has been mired in deep debates-about what reason is, how it works, what are the best tools to model reason, what role normative considerations should play in its study, and, above all, endless debates around a few experimental paradigm such as Wason's selection task or Kahneman and Tversky's conjunction fallacy. If debates are a healthy part of science, the lack of resolution after several decades of work, even when it comes to the interpretation of simple, well-studied problems, suggests that something quite fundamental is wrong with the way reason has been understood so far. The rise of dual process theories over the past 20 years seemed to promise a unified framework allowing different perspective would converge. However, if dual process theories have proven a very successful export-they are now popular in many fields, from moral reasoning to behavioral economics-they are, ironically, in retreat within the psychology of reasoning itself (e.g. Bago & De Neys, 2017;[START_REF] Melnikoff | The mythical number two[END_REF]. Thus, in spite of many brilliant experiments and theoretical insights garnered over the past few decades, we believe the study of human reason is ripe for some serious rethinking, starting from different, and hopefully sturdier, foundations.

One of the strength of our perspective is to precisely situate reason in relation with other cognitive mechanisms. To do so, Part II, "Understanding Inference," develops a taxonomy of cognitive mechanisms, summarized in Figure 1. The circles represent increasingly narrow categories of cognitive mechanisms. The fact that reason is in the center is a mere accident of the fact that reason is the focus of the current work, and an equivalent diagram could be drawn for any other cognitive mechanism. The broadest category in Figure 1 is that of inference. Humans and other animals constantly perform inferences, building on what they already know to draw new conclusions. These inferences allow us to make sense of our perceptual environment, to anticipate the consequences of our actions, to predict what other people will do, to understand what people mean when they speak. By contrast with some dual-process perspectives, we do not believe that humans, or any other animal for that matter, draw most of their inferences by means of some general inferential ability. Instead, humans use a wide variety of specialized inferential mechanisms, each dedicated to helping us solve a distinct problem: At what distance is an object in the visual scene? How much strength will be needed to lift some object? Is this edible? Who would make the most suitable mate? Is this animal dangerous? Fight or flee? How to react to this signal emitted by a conspecific? And so on and so forth. These specialized inferential abilities are partly instinctual, and partly the result of development and learning, with the balance varying from one ability to the next. Plausibly all inferences, in non-human animals, and the vast majority of inferences in humans, never reach awareness-think low-level visual or syntactic processing, motor control, etc. We define intuitions-or intuitive inference-as those inferences which happen to have a conscious output together with specific metacognitive properties, such as a characteristic feeling of selfconfidence (as discussed in Thompson 2014). For example, in a restaurant you might glance at a dish on another table and have an intuition that you'll love it. Even if you have no idea why or how you came to this conclusion, you feel as if the internal, hidden processes that led you to draw it were sound enough.

The next category depicted in Figure 1 is that of intuitions about representations-or metarepresentational inferences. Reason isn't the only human peculiarity. Humans are also the only animal able to fluently represent representations, and indeed humans spend much of their time doing so. Whenever we're around other people, or if we merely think of them, we represent their mental states: what their beliefs, intentions, desires are. When we engage in actual or imagined communication, we process several layers of representations [START_REF] Sperber | Relevance: Communication and cognition[END_REF].

Our first central claim is that reason is 'just' another type of inference. More specifically, reason is a mechanism of metarepresentational intuitive inferences that bears on one type of representations: reasons. This claim is developed in Part III, "Rethinking Reason," in which we suggest that the study of reason (as a cognitive ability) and reasons (justifications, arguments) should be unified-even though they have often been treated separately. Reasons are essentially social. We produce reasons to justify our actions or beliefs, and to convince others. We evaluate others' reasons to decide how much belief revision they warrant. If we can use reasons on our own, in solitary ratiocination, this is only a derivative usage. Moreover, in this view, the study of reason is quite divorced from that of logic (or of any other system of formal rules). Instead of being the foundation of reason, logic is a rhetorical tool that helps us express arguments more clearly by highlighting and often exaggerating the relation between premises and conclusion.

If reason isn't guided by logic, if using reason on our own is a mere byproduct, then what is the function of reason? Our second central claim is that reason mostly serves social functions, more specifically, to exchange justifications, and to exchange arguments.

More than any other primate, humans cooperate, not only with kin, but also with non-kin. This cooperation would not be sustainable if we didn't evaluate other people's reliability as partners in cooperation and in particular their competence and fairness (Baumard, André, & Sperber, 2013). Direct evidence of reliability is provided by the way people behave, but this evidence is limited to one's observations and is typically open to a variety of interpretations. So, we rely massively on evidence provided by others through testimony and gossip. This social evidence, when aggregated, determines a person's reputation. Having a good reputation as a reliable cooperator is a condition of social success and, beyond that, of biological fitness. This gives us a strong incentive to try to protect and improve our reputation by explaining and justifying ourselves. As observers, we have an incentive to evaluate and possibly challenge these self-justifications. Producing justifications and evaluating them is, we claim, one of the two functions of reason.

Another striking feature of humans is the extent to which they communicate. Like cooperation, communication brings its own evolutionary issues: how to avoid being lied to, misled, manipulated. To these ends, we calibrate our trust in others, being more likely to take the word of someone deemed competent and benevolent [START_REF] Mercier | How gullible are we? A review of the evidence from psychology and social science[END_REF][START_REF] Sperber | Epistemic vigilance[END_REF]. However, by relying purely on trust, we are bound to miss out on information that is valuable, but provided by a speaker we don't trust quite enough to change our minds. In this situation, the speaker can produce arguments that, unlike mere testimony, are evaluable on their own merit, independently of the source. Accepting such arguments may lead us to change our mind when trust in the source would not have been strong enough for us to do so. Such exchanges of arguments allows for a much finer grained discrimination between valuable, and inaccurate or harmful messages.

In the past, we had focused on this latter function of reason, developing an argumentative theory of reasoning [START_REF] Mercier | The argumentative theory: Predictions and empirical evidence[END_REF][START_REF] Mercier | Why do humans reason? Arguments for an argumentative theory[END_REF]. Since, in The Enigma of Reason, we claim that reason also serves another social function-namely justification-we prefer to call our current approach to reason interactionist.

Part IV, "What Reason Can and Cannot Do," reviews evidence pertaining to the functioning of human reason, and argues that the evidence is more coherent with our interactionist account, than with other perspectives on reason. If the interactionist account is correct, we should expect reason to exhibit certain features (summarized in Table 1). Given that reason serves very different roles when it produces reasons aimed at others, than when it evaluates reasons others aim at us, we should expect reason to exhibit different traits when it serves each of these roles.

Bias

Quality control When we produce reasons, we should be heavily biased towards our point of view. We're not going to appear more rational by providing reasons why what we did was stupid; we're not going to convince someone by giving them arguments for their point of view or against ours. This explains an otherwise puzzling feature of reason: the myside bias (or confirmation bias, see Mercier, 2016a).

Production of reasons

We might also expect that reason would be able to produce very strong reasons, to better defend ourselves and convince others. However, finding strong reasons is a cognitively demanding task, one that is best accomplished not through brute force, but by paying attention to feedback. In our account, reason evolved as it was used in social, dialogic contexts. In such contexts, if someone isn't convinced by a reason, the natural reaction is for them to provide another reason in turn-typically, a counter-argument. It is then possible for speakers to rely on the feedback provided by their interlocutors in order to provide better reasons, rather than having to find such reasons purely on their own. As a result, we expect the production of reasons to be lazy, but in a smart way: the first reasons we muster can be pretty banal, but we should be able to adapt to the counter-arguments raised by our interlocutors.

The way we evaluate others' reasons-at least when the reasons aim at changing our mindshould be the opposite of the way we produce reasons. We should be able to recognize good reasons, even if they challenge our prior beliefs and come from sources we do not completely trust. Indeed, doing so is, according to us, the very point of reason. And we should be able to reject weak reasons, so as not to be convinced when doing so is not warranted.

These features of reason have several implications. When people reason on their own, they should mostly produce reasons to defend their pre-existing opinions. This explains why a solitary reasoner generally fails to correct their own mistaken intuitions: as reasons pile up to support these intuitions, the reasoner even risks becoming more confident or more polarized. When a solitary reasoner doesn't have a strong intuition to begin with, reason pushes them towards the decision that is most easily justified-whether it is an otherwise good decision or not (a phenomenon known as reason-based choice in the judgment and decision making literature).

By contrast, when people reason with each other, they take turn producing reasons and evaluating others' reasons. Under the right conditions-a small group, with some common incentives but yet disagreeing over some point-discussion and the exchange of reasons works wonders. Those who have the best ideas, or some valuable insight into a problem, can convince the other group members, leading to improvements in performance, sometimes huge ones (for a review of recent evidence, see [START_REF] Mercier | The argumentative theory: Predictions and empirical evidence[END_REF]; see also, [START_REF] Claidière | Argumentation and the diffusion of counterintuitive beliefs[END_REF]. That the exchange of reasons allows good ideas to spread, and performance to increase, has been observed with a wide variety of contents, from logical problems to forecasting or medical decisions.

While Part IV mostly rests on evidence gathered in the lab, Part V, "Reason in the Wild," tackles similar issues, but focusing on other sources of evidence-from anthropology, history, sociology. We start by looking at the cross-culturally robustness of the main features of reason. Is the production of reason biased and lazy in different cultures? Are people everywhere able to make the best of group discussions? By and large, the answer is yes. We then turn to two domains in which reason has been claimed to function in ways that are at odds with our approach. In the domain of morality, we attempt to refute a pessimistic view according to which moral arguments would be essentially inert, showing instead that good reasons can change people's minds, even on highly moral and emotional matters. We then turn to science, often seen as a domain of solitary geniuses figuring out grand theories on their own, and failing to convince their lesser colleagues of their brilliant insights-quite the opposite of what we predict. However, work on the history and sociology of science paints a different picture, one of scientists in constant exchange (or at least revisiting past exchanges and anticipating new ones), who push each other to develop better arguments, and whose theories can rapidly take over a field, as soon as they are well enough supported.

In this book, we thus argue for an original solution to the two enigmas of reason. Reason is uniquely human because it evolved in response to selection pressures uniquely faced by humans-cooperation and communication of an unrivalled scale and complexity. These selection pressures gave rise to inferential mechanisms dedicated to the processing of reasons for social consumption: to exchange arguments and justifications. Reason isn't a superpower, it's just another specialized cognitive mechanism-one that may do wonders but at the social and cultural scale rather than at the individual scale-whose strengths and weaknesses can be explained in light of its function.

Figure 1 .

 1 Figure 1. Categories of mental mechanisms (Figure 1 of The Enigma of Reason)

  Bago, B., & De Neys, W. (2017). Fast logic?: Examining the time course assumption of dual process theory. Cognition, 158, 90-109. Baumard, N., André, J. B.,& Sperber, D. (2013). A mutualistic approach to morality: the evolution of fairness by partner choice.Behavioral and Brain Sciences, 36(01),[59][60][61][62][63][64][65][66][67][68][69][70][71][72][73][74][75][76][77][78]

Table 1 .

 1 The main characteristics of human reason (Figure19of The Enigma of Reason)

	Biased: people mostly	Lazy: people are not very
	produce reasons for their	exigent towards their own
	side	reasons
	Evaluation of others' reasons Unbiased: people accept	Demanding: people are only
	even challenging reasons,	convinced by good enough
	if they are strong enough	reasons

* Hugo Mercier's work is supported by the Agence Nationale de la Recherche, EUR FrontCog ANR-17-EURE-0017. Dan Sperber's work is supported by the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement n° [609819], SOMICS.