Jiří Adámek
email: j.adamek@tu-braunschweig.de

FIXED POINTS OF FUNCTORS -A SHORT ABSTRACT

Fixed points of endofunctors play a central role in program semantics (initial algebras as recursive specification of domains), in coalgebraic theory of systems (terminal coalgebras and coinduction) and in a number of other connections such as iterative theories (rational fixed point). In this survey we present some older and new results on the structure of the three fixed points we have mentioned.

INITIAL ALGEBRAS

The classical example of Σ-algebras as algebras for the polynomial set functor F Σ yields the initial algebra µF Σ = all finite Σ-trees.

This holds for all finitary signatures, whereas for the infinitary ones the initial algebra is formed by all well-founded trees. These are the trees in which every path is finite. The concept of well-foundedness is fundamental for initial algebras. This is a property of coalgebras studied by Osius [START_REF] Osius | Categorical set theory: a characterization of the category of sets[END_REF] and Taylor [START_REF] Taylor | Towards a unified treatment of induction i: the general recursion theorem[END_REF]. In [4] we have proved that for all set functors F the initial algebra coincides with the terminal well-founded coalgebra. And every fixed point of F has a largest well-founded part which is the initial algebra of F , see [START_REF] Adámek | Initial algebras and terminal coalgebras[END_REF] The iterative construction of µF as F i (0) (for some ordinal i), introduced in [START_REF] Adámek | Free algebras and automata realizations in the language of categories[END_REF], converges for every set functor with a fixed point, see [START_REF] Trnková | Free algebras, input processes and free monads[END_REF]. Moreover the least such ordinal i is an infinite regular cardinal or at most 3, as proved in [START_REF] Adámek | Initial algebras and terminal coalgebras in many-sorted sets[END_REF]. In contrast, on the category of many-sorted sets convergence can take place at any ordinal, and on the category of graphs endofunctors exist having an initial algebra although the iterative construction does not converge, see [START_REF] Adámek | Initial algebras and terminal coalgebras in many-sorted sets[END_REF].

Most of the above results extend from set functors to enfodunctors of "reasonable" categories preserving monomorphisms. For example locally finitely presentable categories whose initial object is simple are "reasonable".

The importance of terminal coalgebras as systems was demonstrated by Rutten in his fundamental paper [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF].

A number of classical examples are special cases of the following:

νF Σ = all Σ-trees.
The case of automata with n inputs, H n X = X n × {0, 1}, is an example where Σ consists of two n-ary operations (and Σ-trees just represent languages in n * ). And streams, F X = A × X + B, correspond to unary operations in A and constants in B.

In case of set functors, it is useful to work with pointed coalgebras. E.g., the classical automata are pointed coalgebras for H n . Definition 1. A well-pointed coalgebra is a pointed coalgebra having no proper subobject and no proper quotient.

Thus minimal automata are precisely the well-pointed coalgebras for H n . Let T be the collection of all well-pointed coalgebras up to isomorphism. If F is a set functor preserving intersections, every pointed coalgebra has a canonical "minimization" to a well-pointed one. This yields a coalgebra structure on T . And in [4] we presented the following characterizations: νF = all well-pointed coalgebras(up to isomoprhism) and µF = all well-founded well-pointed coalgebras (up to isomoprhism).

"The dual of the iterative initial-algebra construction, i.e. the cochain F i (1) as a construction of νF , was first explicitly considered by Barr [START_REF] Barr | Terminal coalgebras in well-founded set theory[END_REF]. In contrast to the initial chain the convergence does not always happen at a cardinal: Worrell proved that for the finite power-set functor that cochain converges in ω +ω steps. And for all λ-accessible set functors (i.e., those preserving λ-filtered colimits), he proved that the construction converges in λ + λ steps or sooner, see [START_REF] Worrell | On the final sequence of a finitary set functor[END_REF]. Until recently, for uncountable λ, no example has been known where the full λ + λ steps are actually needed. Such an example is the functor of all λ-generated filters, see [START_REF] Adámek | Fixed points of set functors: how many iterations are needed?[END_REF].

An important classical result concerns enriched endofunctors of the cartesian closed category CPO (of posets with directed joins and a bottom and strict continuous maps): Smyth and Plotkin proved in [START_REF] Smyth | Category-theoretical solution of recursive domain equations[END_REF] that the terminal coalgebra equals the initial algebra, and both constructions converge in ω steps. This is based on the limit-colimit coincidence for embedding-projection pairs of Scott. In [START_REF] Adámek | Initial algebras and terminal coalgebras[END_REF] we prove that for the (much wider) class of endofunctors that are just locally monotone the existence of a fixed point implies that the terminal coalgebra exists and equals the initial algebra.

RATIONAL FIXED POINT

This (much younger) fixed point arose in the study of iterative algebras. These are algebras A that have a unique solution of every finite guarded system of recursive equations (with parameters in A). In [START_REF] Adámek | Iterative algebras at work[END_REF] we proved that every finitary set functor has an initial iterative algebra which is a fixed point, notation: ρF . And we called this the rational fixed point. Classical examples: for automata as coalgebras we have ρH n = all regular languages in n * , and for general signatures ρF Σ = all rational Σ-trees, that is, trees that have, up to isomorphism, only finitely many subtrees.

The rational fixed point can be described as the filtered colimit of all finite coalgebras. This has inspired Milius [START_REF] Milius | A sound and complete calculus for finite stream circuits[END_REF] to define locally finite coalgebras for a set functor as coalgebras that are directed unions of finite subcoalgebras. And then he proved that ρF = the terminal locally finite coalgebra.

In a complete analogy to the above characterization of the initial and terminal fixed point we have that ρF = all finite well-pointed coalgebras (up to isomorphism).

All the above generalizes easily to finitary endofunctors of all finitely locally presentable categories.

Can we play the same game with countable sets in place of finite ones? No, only finite sets yield something new: the terminal locally countable coalgebra is all of νF , see [START_REF] Adámek | Iterative algebras at work[END_REF].


Ekaterina Komendantskaya

John Power

Category theoretic semantics for theorem proving in logic programming: embracing the laxness

Keywords: Logic programming, coalgebra, term-matching resolution, coinductive derivation tree, Lawvere theories, lax transformations, Kan extensions

A propositional logic program P may be identified with a P f P f -coalgebra on the set of atomic propositions in the program. The corresponding C(P f P f )-coalgebra, where C(P f P f ) is the cofree comonad on P f P f , describes derivations by resolution. Using lax semantics, that correspondence may be extended to a class of first-order logic programs without existential variables. The resulting extension captures the proofs by term-matching resolution in logic programming. Refining the lax approach, we further extend it to arbitrary logic programs. We also exhibit a refinement of Bonchi and Zanasi's saturation semantics for logic programming that complements lax semantics.

Introduction

Consider the following two logic programs.

Example 1. ListNat (for lists of natural numbers) denotes the logic program 1. nat(0) ← 2. nat(s(x)) ← nat(x) 3. list(nil) ← 4. list(cons(x, y)) ← nat(x), list(y)

A critical difference between ListNat and GC is that in the latter, which is a leading example in Sterling and Shapiro's book [START_REF] Sterling | The art of Prolog[END_REF], there is a variable z in the tail of the second clause that does not appear in its head. The category theoretic consequences of that fact are the central concern of this paper.

It has long been observed, e.g., in [START_REF] Bonchi | Reactive systems, (semi-)saturated semantics and coalgebras on presheaves[END_REF][START_REF] Comini | A theory of observables for logic programs[END_REF], that logic programs induce coalgebras, allowing coalgebraic modelling of their operational semantics. In [START_REF] Komendantskaya | Coalgebraic semantics for parallel derivation strategies in logic programming[END_REF], we developed the idea for variable-free logic programs as follows. Using the definition of a logic program [START_REF] Lloyd | Foundations of Logic Programming[END_REF], given a set of atoms At, one can identify a variable-free logic program P built over At with a P f P f -coalgebra structure on At, where P f is the finite powerset functor on Set: each atom is the head of finitely many clauses in P , and the body of each clause contains finitely many atoms. Our main result was that if C(P f P f ) is the cofree comonad on P f P f , then, given a logic program P qua P f P f -coalgebra, the corresponding C(P f P f )-coalgebra structure characterises the and-or derivation trees generated by P , cf [START_REF] Gupta | Optimal implementation of and-or parallel prolog[END_REF].

This result has proved to be stable, not only having been further developed by us [START_REF] Komendantskaya | Coalgebraic Logic Programming:from Semantics to Implementation[END_REF][START_REF] Komendantskaya | Exploiting Parallelism in Coalgebraic Logic Programming[END_REF][START_REF] Johann | Structural Resolution for Logic Programming[END_REF][START_REF] Fu | A Type-Theoretic Approach to Resolution[END_REF][START_REF] Fu | Proof Relevant Corecursive Resolution[END_REF], but also forming the basis for Bonchi and Zanasi's saturation semantics for logic programming (LP) [START_REF] Bonchi | Saturated semantics for coalgebraic logic programming[END_REF][START_REF] Bonchi | Bialgebraic Semantics for Logic Programming[END_REF]. In Sections 2, 3, we give an updated account of the work, with updated definitions, proofs and detailed examples, to start our semantic analysis of derivations and proofs in LP.

In [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF], we extended our analysis from variable-free logic programs to arbitrary logic programs. Following [START_REF] Amato | On the algebraic structure of declarative programming languages[END_REF][START_REF] Bonchi | Reactive systems, (semi-)saturated semantics and coalgebras on presheaves[END_REF][START_REF] Bruni | An interactive semantics of logic programming[END_REF][START_REF] Kinoshita | A fibrational semantics for logic programs[END_REF], given a signature Σ of function symbols, we let L Σ denote the Lawvere theory generated by Σ, and, given a logic program P with function symbols in Σ, we considered the functor category [L op Σ , Set], extending the set At of atoms in a variable-free logic program to the functor from L op Σ to Set sending a natural number n to the set At(n) of atomic formulae with at most n variables generated by the function symbols in Σ and the predicate symbols in P . We sought to model P by a [L op Σ , P f P f ]-coalgebra p : At -→ P f P f At that, at n, takes an atomic formula A(x 1 , . . . , x n ) with at most n variables, considers all substitutions of clauses in P into clauses with variables among x 1 , . . . , x n whose head agrees with A(x 1 , . . . , x n ), and gives the set of sets of atomic formulae in antecedents, mimicking the construction for variable-free logic programs. Unfortunately, that idea was too simple.

Consider the logic program ListNat, i.e., Example 1. There is a map in L Σ of the form 0 → 1 that models the nullary function symbol 0. So, naturality of the map p : At -→ P f P f At in [L op Σ , Set] would yield commutativity of the diagram

At(1) p 1 -P f P f At(1)
At(0) At(0) ? p 0 -P f P f At(0)

P f P f At(0)
? But consider nat(x) ∈ At(1): there is no clause of the form nat(x) ← in ListNat, so commutativity of the diagram would imply that there cannot be a clause in ListNat of the form nat(0) ← either, but in fact there is one.

At that point, proposed resolutions diverged: at CALCO in 2011, we proposed one approach using lax transformations [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF], then at CALCO 2013, Bonchi and Zanasi proposed another, using saturation semantics [START_REF] Bonchi | Saturated semantics for coalgebraic logic programming[END_REF], an example of the positive interaction generated by CALCO! In fact, as we explain in Section 6, the two approaches may be seen as complementary rather than as alternatives. First we shall describe our approach.

We followed the standard category theoretic technique of relaxing the naturality condition on p to a subset condition, e.g., as in [START_REF] Benabou | Introduction to bicategories[END_REF][START_REF] Blackwell | Two-dimensional monad theory[END_REF][START_REF] Jifeng | Categorical semantics for programming languages[END_REF][START_REF] Kelly | Coherence theorems for lax algebras and for distributive laws[END_REF][START_REF] Kinoshita | Lax naturality through enrichment[END_REF], so that, in general, given a map in L Σ of the form f : n → m, the diagram

At(m) p m -P f P f At(m) At(n) At(f ) ? p n -P f P f At(n) P f P f At(f ) ?
need not commute, but rather the composite via P f P f At(m) need only yield a subset of that via At(n). So, for example, p 1 (nat(x)) could be the empty set while p 0 (nat(0)) could be non-empty in the semantics for ListNat as required.

We extended Set to P oset in order to express the laxness, and we adopted established category theoretic research on laxness, notably that of [START_REF] Kelly | Coherence theorems for lax algebras and for distributive laws[END_REF], in order to prove that a cofree comonad exists and behaves as we wished.

For a representative class of logic programs, the above semantics describes derivations arising from restricting the usual SLD-resolution used in LP to termmatching resolution, cf. [START_REF] Komendantskaya | Coalgebraic derivations in logic programming[END_REF][START_REF] Komendantskaya | Coalgebraic Logic Programming:from Semantics to Implementation[END_REF]. As transpired in further studies [START_REF] Fu | A Type-Theoretic Approach to Resolution[END_REF][START_REF] Johann | Structural Resolution for Logic Programming[END_REF], this particular restriction to resolution rule captures the theorem-proving aspect of LP as opposed to the problem-solving aspect captured by SLD-resolution with unification. We explain this idea in Section 2. Derivation trees arising from proofs by term-matching resolution were called coiductive trees in [START_REF] Komendantskaya | Coalgebraic derivations in logic programming[END_REF][START_REF] Komendantskaya | Coalgebraic Logic Programming:from Semantics to Implementation[END_REF] to mark their connection to the coalgebraic semantics.

Categorical semantics introduced in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF] worked well for ListNat, allowing us to model its coinductive trees, as we show in Section 4 (It was not shown explicitly in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF]). However, it does not work well for GC, the key difference being that, in ListNat, no variable appears in a tail of a clause that does not also appear in its head, i.e., clauses in ListNat contain no existential variables. In contrast, although not expressed in these terms in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF], we were unable to model the coinductive trees generated by GC because it is an existential program, i.e. program containing clauses with existential variables. We worked around the problems in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF], but only inelegantly.

We give an updated account of [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF] in Section 4, going beyond [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF] to explain how coinductive trees for logic programs without existential variables are modelled, and explaining the difficulty in modelling coinductive semantics for arbitrary logic programs. We then devote Section 5 of the paper to resolution of the difficulty, providing lax semantics for coinductive trees generated by arbitrary logic progams.

In contrast to this, Bonchi and Zanasi, concerned by the complexity involved with laxness, proposed the use of saturation, following [START_REF] Bonchi | Reactive systems, (semi-)saturated semantics and coalgebras on presheaves[END_REF], to provide an alternative category theoretic semantics [START_REF] Bonchi | Saturated semantics for coalgebraic logic programming[END_REF][START_REF] Bonchi | Bialgebraic Semantics for Logic Programming[END_REF]. Saturation is indeed an established and useful construct, as Bonchi and Zanasi emphasised [START_REF] Bonchi | Saturated semantics for coalgebraic logic programming[END_REF][START_REF] Bonchi | Bialgebraic Semantics for Logic Programming[END_REF], with a venerable tradition, and, as they say, laxness requires careful calculation, albeit much less so in the setting of posets than that of categories. On the other hand, laxness is a standard part of category theory, one that has been accepted by computer scientists as the need has arisen, e.g., by He Jifeng and Tony Hoare to model data refinement [START_REF] Jifeng | Categorical semantics for programming languages[END_REF][START_REF] Jifeng | Data refinement in a categorical setting[END_REF][START_REF] Kinoshita | Lax naturality through enrichment[END_REF][START_REF] Power | An algebraic formulation for data refinement[END_REF]. More fundamentally, saturation can be seen as complementary to the use of laxness rather than as an alternative to it, as we shall explain in Section 6. This reflects the important connection between the theorem proving and problem solving aspects of proof search in LP, as Section 2 further explains. So we would suggest that both approaches are of value, with the interaction between them meriting serious consideration.

Saturation inherently yields a particular kind of compositionality, but one loses the tightness of the relationship between semantic model and operational behaviour. The latter is illustrated by the finiteness of branching in a coinductive tree, in contrast to the infinity of possible substitutions, which are inherent in saturation. To the extent that it is possible, we would like to recover operational semantics from the semantic model, along the lines of [START_REF] Plotkin | Adequacy for Algebraic Effects[END_REF], requiring maintenance of intensionality where possible. We regard the distinction between ListNat and GC as a positive feature of lax semantics, as a goal of semantics is to shed light on the critical issues of programming, relation of existential programs to theorem-proving in LP being one such [START_REF] Fu | A Type-Theoretic Approach to Resolution[END_REF]. So we regard Section 6 as supporting both lax and saturation semantics, the interaction between them shedding light on logic programming.

Background: theorem proving in LP

A signature Σ consists of a set F of function symbols f, g, . . . each equipped with an arity. Nullary (0-ary) function symbols are constants. For any set Var of variables, the set T er(Σ) of terms over Σ is defined inductively as usual:

x ∈ T er(Σ) for every x ∈ Var .

-If f is an n-ary function symbol (n ≥ 0) and t 1 , . . . , t n ∈ T er(Σ), then f (t 1 , . . . , t n ) ∈ T er(Σ).

A substitution over Σ is a total function σ : Var → Term(Σ). Substitutions are extended from variables to terms as usual: if t ∈ Term(Σ) and σ is a substitution, then the application σ(t) is a result of applying σ to all variables in t. A substitution σ is a unifier for t, u if σ(t) = σ(u), and is a matcher for t against u if σ(t) = u. A substitution σ is a most general unifier (mgu) for t and u if it is a unifier for t and u and is more general than any other such unifier. A most general matcher (mgm) σ for t against u is defined analogously.

In line with LP tradition [START_REF] Lloyd | Foundations of Logic Programming[END_REF], we also take a set P of predicate symbols each equipped with an arity. It is possible to define logic programs over terms only, in line with term-rewriting (TRS) tradition [START_REF]Term Rewriting Systems[END_REF], as we do in [START_REF] Johann | Structural Resolution for Logic Programming[END_REF], but we will follow the usual LP tradition here. This gives us the following inductive definitions of the sets of atomic formulae, Horn clauses and logic programs (we also include the definition of terms here for convenience): In what follows, we will use letters A, B, C, D, possibly with subscripts, to refer to elements of At.

Given a logic program P , we may ask whether a certain atom is logically entailed by P . E.g., given the program ListNat we may ask whether list(cons(0, nil)) is entailed by ListNat. The following rule, which is a restricted form of the famous SLD-resolution, provides a semi-decision procedure to derive the entailment: Definition 2 (Term-matching (TM) Resolution).

P [ ]

P σA1 • • • P σAn P σA if (A ← A1, . . . , An) ∈ P
In contrast, the SLD-resolution rule could be presented in the following form: B 1 , . . . , B j , . . . , B n ; P σB 1 , . . . , σA 1 , . . . , σA n , . . . , σB n , if (A ← A 1 , . . . , A n ) ∈ P , and σ is the mgu of A and B j . The derivation for A succeeds when A ; P [ ]; we use ; * P to denote several steps of SLD-resolution. At first sight, the difference between TM-resolution and SLD-resolution seems to be that of notation. Indeed, both ListN at list(cons(0, nil)) and list(cons(0, nil)) ; * ListN at [ ] by the above rules (see also Figure 1). However, ListN at list(cons(x, y)) whereas list(cons(x, y)) ; * ListN at [ ]. And, even more mysteriously, GC connected(x, y) while connected(x, y) ; GC [ ].

As it turns out, TM-resolution reflects the theorem proving side of LP: rules of Definition 2 can be used to semi-decide whether a given term t is entailed by P . In contrast, SLD-resolution reflects the problem solving aspect of LP: using the SLD-resolution rule, one asks whether, for a given t, a substitution σ can be found such that P σ(t). There is a subtle but important difference between these two aspects of proof search.

For example, when considering the successful derivation list(cons(x, y))

; * ListN at [ ],
we assume that list(cons(x, y)) holds only relative to a computed substitution, e.g. x → 0, y → nil. Of course this distinction is natural from the point of view of theorem proving: list(cons(x, y)) is not a "theorem" in this generality, but its special case, list(cons(0, nil)), is. Thus, ListN at list(cons(0, nil)) but ListN at list(cons(x, y)) (see also Figure 1). Similarly, connected(x, y) ; GC [ ] should be read as: connected(x, y) holds relative to the computed substitution y → x.

According to the soundness and completeness theorems for SLD-resolution [START_REF] Lloyd | Foundations of Logic Programming[END_REF], the derivation ; has existential meaning, i.e. when list(cons(x, y)) ; *

ListN at

[ ], the succeeded goal list(cons(x, y)) is not meant to be read as universally quantified over x an y. On the contrary, TM-resolution proves a universal statement. That is, GC connected(x, x) reads as: connected(x, x) is entailed by GC for any x.

Much of our recent work has been devoted to formal understanding of the relation between the theorem proving and problem solving aspects of LP [START_REF] Johann | Structural Resolution for Logic Programming[END_REF][START_REF] Fu | A Type-Theoretic Approach to Resolution[END_REF]. The type-theoretic semantics of TM-resolution, given by "Horn clauses as types, λ-terms as proofs" is given in [START_REF] Fu | A Type-Theoretic Approach to Resolution[END_REF][START_REF] Fu | Proof Relevant Corecursive Resolution[END_REF].

Definition 2 gives rise to derivation trees. E.g. the derivation (or, equivalently, the proof) for ListN at list(cons(0, nil)) can be represented by the following derivation tree:

list(cons(0, nil)) nat(0) [ ] list(nil) [ ]
In general, given a term t and a program P , more than one derivation for P t is possible. For example, if we add a fifth clause to program ListN at: 5. list(cons(0, x)) ← list(x) then yet another, alternative, proof is possible for the extended program: ListN at + list(cons(0, nil)) via the clause 5:

list(cons(0, nil)) list(nil) [ ]
To reflect the choice of derivation strategies at every stage of the derivation, we can introduce a new kind of nodes, or-nodes. For our example, this would give us the tree shown in Figure 1, note the •-nodes.

This intuition is made precise in the following definition of a coinductive tree, which first appeared in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF][START_REF] Komendantskaya | Coalgebraic Logic Programming:from Semantics to Implementation[END_REF] and was later refined in [START_REF] Johann | Structural Resolution for Logic Programming[END_REF] under the name of a rewriting tree. Note the use of mgms (rather than mgus) in the last item.

Definition 3 (Coinductive tree). Let P be a logic program and A be an atomic formula. The coinductive tree for A is the possibly infinite tree T satisfying the following properties.

-A is the root of T -Each node in T is either an and-node or an or-node -Each or-node is given by • -Each and-node is an atom -For every and-node A occurring in T , if there exist exactly m > 0 distinct clauses C 1 , . . . , C m in P (a clause C i has the form

B i ← B i 1 , . . . , B i ni for list(cons(0, nil)) nat(0) [ ] list(nil) [ ] list(nil) [ ] list(cons(x, y)) nat(x) list(y)
Fig. 1. Left: a coinductive tree for list(cons(0, nil)) and the extended program ListN at + . Right: a coinductive tree for list(cons(x, y)) and ListN at + . The •-nodes mark different clauses applicable to every atom in the tree.

some n i ), such that A = B 1 θ 1 = . . . = B m θ m , for mgms θ 1 , . . . , θ m , then
A has exactly m children given by or-nodes, such that, for every i ∈ m, the i-th or-node has n i children given by and-nodes

B i 1 θ i , . . . , B i ni θ i .
Coinductive trees provide a convenient model for proofs by TM-resolution.

Let us make one final observation on TM-resolution. Generally, given a program P and an atom t, one can prove that t ; * P [ ] with computed substitution σ iff P σt.

This simple fact may give an impression that proofs (and corresponding coinductive trees) for TM-resolution are in some sense fragments of reductions by SLD-resolution. Compare e.g. the right-hand tree of Figure 1 before substitution and a grown left-hand tree obtained after the substitution. In this case, we could emulate the problem solving aspect of SLD-resolution by using coinductive trees and allowing to apply substitutions within coinductive trees, as was proposed in [START_REF] Komendantskaya | Coalgebraic derivations in logic programming[END_REF][START_REF] Johann | Structural Resolution for Logic Programming[END_REF][START_REF] Fu | A Type-Theoretic Approach to Resolution[END_REF]. Such intuition would hold perfectly for e.g. ListNat, but would not hold for existential programs: although there is a one step SLD-derivation for connected(x, y) ; GC [ ] (with y → x), TM-resolution proof for connected(x, y) diverges and gives rise to the following infinite coinductive tree: connected(x, y) edge(x, z) connected(z, y) edge(x, z1) connected(z1, y) . . . Not only the proof for GC connected(x, y) is not in any sense a fragment of the derivation connected(x, y) ; GC [ ], but it also takes larger (i.e. infinite) signature. Thus, operational semantics of TM-resolution and SLD-resolution can be very different for existential programs: both in aspects of termination and signature size.

This problem is orthogonal to non-termination. Consider the non-terminating (but not existential) program Bad: bad(x) ← bad(x) For Bad, operational behavior of TM-resolution and SLD-resolution are similar: derivations with both do not terminate and require finite signature. Once again, such programs can be analysed using similar coinductive methods in TM-and SLD-resolution [START_REF] Fu | Proof Relevant Corecursive Resolution[END_REF][START_REF] Simon | Co-logic programming: Extending logic programming with coinduction[END_REF].

The problems caused by existential variables are known in the literature on theorem proving and term-rewriting [START_REF]Term Rewriting Systems[END_REF]. In TRS [START_REF]Term Rewriting Systems[END_REF], existential variables are not allowed to appear in rewriting rules, and in type inference based on term rewriting or TM-resolution, the restriction to non-existential programs is common [START_REF] Jones | Type classes: An exploration of the design space[END_REF].

So theorem-proving, in contrast to problem-solving, is modelled by termmatching; term-matching gives rise to coinductive trees; and as explained in the introduction and, in more detail, later, coinductive trees give rise to laxness. So in this paper, we use laxness to model coinductive trees, and thereby theoremproving in LP, and relate our semantics with Bonchi and Zanasi's work, which we believe models primarily problem-solving aspect of logic programming.

Categorical semantics for existential programs, which are known to be challenging for theorem proving, is the main contribution of Section 5 and this paper.

Modelling coinductive trees for variable-free logic programs

In this section, we recall and develop the work of [START_REF] Komendantskaya | Coalgebraic semantics for parallel derivation strategies in logic programming[END_REF] and in particular we restrict our semantics to variable-free logic programs, i.e. we take V ar = ∅ in Definition 1. Variable-free logic programs are operationally equivalent to propositional logic programs, as substitutions play no role in derivations. In this (propositional) setting, coinductive trees coincide with the and-or derivation trees known in the LP literature [START_REF] Gupta | Optimal implementation of and-or parallel prolog[END_REF].

Proposition 1. For any set At, there is a bijection between the set of variablefree logic programs over the set of atoms At and the set of P f P f -coalgebra structures on At, where P f is the finite powerset functor on Set.

Theorem 1. Let C(P f P f ) denote the cofree comonad on P f P f . Then, for p :

At -→ P f P f (At), the corresponding C(P f P f )-coalgebra p : At -→ C(P f P f )(At)
sends an atom A to the coinductive tree for A.

Proof. Applying the work of [START_REF] Worrell | Terminal sequences for accessible endofunctors[END_REF] to this setting, the cofree comonad is in general determined as follows:

C(P f P f )(At) is the limit of the diagram . . . -→ At × P f P f (At × P f P f (At)) -→ At × P f P f (At) -→ At.
with maps determined by the projection π 0 : At × P f P f (At) -→ At, with applications of the functor At × P f P f (-) to it. Putting At 0 = At and At n+1 = At × P f P f At n , and defining the cone

p 0 = id : At -→ At(= At 0 ) p n+1 = id, P f P f (p n ) • p : At -→ At × P f P f At n (= At n+1 )
the limiting property of the diagram determines the coalgebra p : At -→ C(P f P f )(At). The image p(A) of an atom A is given by an element of the limit, equivalently a map from 1 into the limit, equivalently a cone of the diagram over 1.

To give the latter is equivalent to giving an element A 0 of At, specifically p 0 (A) = A, together with an element A 1 of At × P f P f (At), specifically p 1 (A) = (A, p 0 (A)) = (A, p(A)), together with an element A 2 of At×P f P f (At×P f P f (At)), etcetera. The definition of the coinductive tree for A is inherently coinductive, matching the definition of the limit, and with the first step agreeing with the definition of p. Thus it follows by coinduction that p(A) can be identified with the coinductive tree for A. Then p 0 (A) = A, which is the root of the coinductive tree for A.

Then p 1 (A) = (A, p(A)) = (A, {{B, C}, {B, D}}), which consists of the same information as in the first three levels of the coinductive tree for A, i.e., the root A, two or-nodes, and below each of the two or-nodes, nodes given by each atom in each antecedent of each clause with head A in the logic program P : nodes marked B and C lie below the first or-node, and nodes marked B and D lie below the second or-node, exactly as p 1 (A) describes.

Continuing, note that p 1 (D) = (D, p(D)) = (D, {{A, C}}). So

p 2 (A) = (A, P f P f (p 1 )(p(A))) = (A, P f P f (p 1 )({{B, C}, {B, D}})) = (A, {{(B, ∅), (C, ∅)}, {(B, ∅), (D, {{A, C}})}})
which is the same information as that in the first five levels of the coinductive tree for A: p 1 (A) provides the first three levels of p 2 (A) because p 2 (A) must map to p 1 (A) in the cone; in the coinductive tree, there are two and-nodes at level 3, labelled by A and C. As there are no clauses with head B or C, no or-nodes lie below the first three of the and-nodes at level 3. However, there is one or-node lying below D, it branches into and-nodes labelled by A and C, which is exactly as p 2 (A) tells us.

For pictures of such trees, see [START_REF] Komendantskaya | Coalgebraic Logic Programming:from Semantics to Implementation[END_REF]. existential variables

We now lift the restriction on V ar = ∅ in Definition 1, and consider first-order terms and atoms in full generality, however, we restrict the definition of clauses in Definition 1 to those not containing existential variables.

The Lawvere theory L Σ generated by a signature Σ is (up to isomorphism, as there are several equivalent formulations) the category defined as follows: ob(L Σ ) is the set of natural numbers. For each natural number n, let x 1 , . . . , x n be a specified list of distinct variables. Define L Σ (n, m) to be the set of mtuples (t 1 , . . . , t m ) of terms generated by the function symbols in Σ and variables x 1 , . . . , x n . Define composition in L Σ by substitution.

One can readily check that these constructions satisfy the axioms for a category, with L Σ having strictly associative finite products given by the sum of natural numbers. The terminal object of L Σ is the natural number 0.

Example 4. Consider ListNat. The constants O and nil are maps from 0 to 1 in L Σ , s is modelled by a map from 1 to 1, and cons is modelled by a map from 2 to 1. The term s(0) is the map from 0 to 1 given by the composite of the maps modelling s and 0.

Given an arbitrary logic program P with signature Σ, we can extend the set At of atoms for a variable-free logic program to the functor At : L op Σ → Set that sends a natural number n to the set of all atomic formulae, with variables among x 1 , . . . , x n , generated by the function symbols in Σ and by the predicate symbols in P . A map f : n → m in L Σ is sent to the function At(f ) : At(m) → At(n) that sends an atomic formula A(x 1 , . . . , x m ) to A(f 1 (x 1 , . . . , x n )/x 1 , . . . , f m (x 1 , . . . , x n )/x m ), i.e., At(f ) is defined by substitution.

As explained in the Introduction and in [START_REF] Komendantskaya | Coalgebraic semantics for parallel derivation strategies in logic programming[END_REF], we cannot model a logic program by a natural transformation of the form p : At -→ P f P f At as naturality breaks down, e.g., in ListNat. So, in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF][START_REF] Komendantskaya | Coalgebraic Logic Programming:from Semantics to Implementation[END_REF], we relaxed naturality to lax naturality. In order to define it, we extended At : L op Σ → Set to have codomain P oset by composing At with the inclusion of Set into P oset. Mildly overloading notation, we denote the composite by At : L op Σ → P oset. Definition 4. Given functors H, K : L op Σ -→ P oset, a lax transformation from H to K is the assignment to each object n of L Σ , of an order-preserving function α n : Hn -→ Kn such that for each map f : n -→ m in L Σ , one has (Kf )(α m ) ≤ (α n )(Hf ), pictured as follows:

Hm α m -Km ≥ Hn Hf ? α n -Kn Kf ?
Functors and lax transformations, with pointwise composition, form a locally ordered category denoted by Lax(L op Σ , P oset). Such categories and generalisations have been studied extensively, e.g., in [START_REF] Benabou | Introduction to bicategories[END_REF][START_REF] Blackwell | Two-dimensional monad theory[END_REF][START_REF] Kelly | Coherence theorems for lax algebras and for distributive laws[END_REF][START_REF] Kinoshita | Lax naturality through enrichment[END_REF]. Definition 5. Define P f : P oset -→ P oset by letting P f (P ) be the partial order given by the set of finite subsets of P , with A ≤ B if for all a ∈ A, there exists b ∈ B for which a ≤ b in P , with behaviour on maps given by image. Define P c similarly but with countability replacing finiteness.

We are not interested in arbitrary posets in modelling logic programming, only those that arise, albeit inductively, by taking subsets of a set qua discrete poset. So we gloss over the fact that, for an arbitrary poset P , Definition 5 may yield factoring, with the underlying set of P f (P ) being a quotient of the set of subsets of P . It does not affect the line of development here.

Example 5. Modelling Example 1, ListNat generates a lax transformation of the form p : At -→ P f P f At as follows: At(n) is the set of atomic formulae in ListN at with at most n variables.

For example, At(0) consists of nat(0), nat(nil), list(0), list(nil), nat(s(0)), nat(s(nil)), list(s(0)), list(s(nil)), nat(cons(0, 0)), nat(cons(0, nil)), nat(cons(nil, 0)), nat(cons(nil, nil)), etcetera.

Similarly, At(1) includes all atomic formulae containing at most one (specified) variable x, thus all the elements of At(0) together with nat(x), list(x), nat(s(x)), list(s(x)), nat(cons(0, x)), nat(cons(x, 0)), nat(cons(x, x)), etcetera.

The function p n : At(n) -→ P f P f At(n) sends each element of At(n), i.e., each atom A(x 1 , . . . , x n ) with variables among x 1 , . . . , x n , to the set of sets of atoms in the antecedent of each unifying substituted instance of a clause in P with head for which a unifying substitution agrees with A(x 1 , . . . , x n ).

Taking n = 0, nat(0) ∈ At(0) is the head of one clause, and there is no other clause for which a unifying substitution will make its head agree with nat(0). The clause with head nat(0) has the empty set of atoms as its tail, so p 0 (nat(0)) = {∅}.

Taking n = 1, list(cons(x, 0)) ∈ At(1) is the head of one clause given by a unifying substititution applied to the final clause of ListNat, and accordingly p 1 (list(cons(x, 0))) = {{nat(x), list(0)}}.

The family of functions p n satisfy the inequality required to form a lax transformation precisely because of the allowability of substitution instances of clauses, as in turn is required to model logic programming. The family does not satisfy the strict requirement of naturality as explained in the introduction. Modulo possible renaming of variables, the head of the clause, i.e., the atom connected(x, y), lies in At(2) as it has two variables. However, the tail does not lie in P f P f At(2) as the tail has three variables rather than two.

We dealt with that inelegantly in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF]: in order to allow p 2 (connected(x, y)) to model GC in any reasonable sense, we allowed substitutions for z by any term on x, y on the basis that there is no unifying such, so we had better allow all possibilities. So, rather than modelling the clause directly, recalling that At(2) ⊆ At(3) ⊆ At(4), etcetera, modulo renaming of variables, we put p2(connected(x, y)) = {{edge(x, x), connected(x, y)}, {edge(x, y), connected(y, y)}} p3(connected(x, y)) = {{edge(x, x), connected(x, y)}, {edge(x, y), connected(y, y)}, {edge(x, z), connected(z, y)}} p4(connected(x, y)) = {{edge(x, x), connected(x, y)}, {edge(x, y), connected(y, y)}, {edge(x, z), connected(z, y)}, {edge(x, w), connected(w, y)}} etcetera: for p 2 , as only two variables x and y appear in any element of P f P f At(2), we allowed substitution by either x or y for z; for p 3 , a third variable may appear in an element of P f P f At(3), allowing an additional possible subsitution; for p 4 , a fourth variable may appear, etcetera.

Countability arises if a unary symbol s is added to GC, as in that case, for p 2 , not only did we allow x and y to be substituted for z, but we also allowed s n (x) and s n (y) for any n > 0, and to do that, we replaced P f P f by P c P f , allowing for the countably many possible substitutions.

Those were inelegant decisions, but they allowed us to give some kind of model of all logic programs. We now turn to the relationship between the lax transformation p : At -→ P c P f At modelling a logic program P and p : At -→ C(P c P f )At, the corresponding coalgebra for the cofree comonad C(P c P f ) on P c P f . We recall the central abstract result of [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF], the notion of an "oplax" map of coalgebras being required to match that of lax transformation. Notation of the form H-coalg refers to coalgebras for an endofunctor H, while notation of the form C-Coalg refers to coalgebras for a comonad C. The subscript oplax refers to oplax maps, and given an endofunctor E on P oset, the notation Lax(L op Σ , E) denotes the endofunctor on Lax(L op Σ , P oset) given by post-composition with E; similarly for a comonad. Theorem 2. For any locally ordered endofunctor E on P oset, if C(E) is the cofree comonad on E, then there is a canonical isomorphism

Lax(L op Σ , E)-coalg oplax Lax(L op Σ , C(E))-Coalg oplax Corollary 1. Lax(L op Σ , C(P c P f )) is the cofree comonad on Lax(L op Σ , P c P f ).
Corollary 1 gives a bijection between lax transformations p : At -→ P c P f At and lax transformations p : At -→ C(P c P f )At subject to the two conditions required of a coalgebra of a comonad. Subject to the routine replacement of the outer copy of P f by P c in the construction in Theorem 1, the same construction, if understood pointwise, extends to this setting, i.e., if one uniformly replaces At by At(n) in the construction of Theorem 1, and replaces the outer copy of P f by P c , one obtains a description of C(P c P f )At(n) together with the construction of p n from p n . That is fine for ListNat, modelling the coinductive trees generated by ListNat, the same holding for any logic program without existential variables, but for GC, as explained in Example 6, p did not model the clause connected(x, y) ← edge(x, z), connected(z, y) directly, and so its extension a fortiori could not model the coinductive trees generated by connected(x, y).

For arbitrary logic programs, p(A(x 1 , . . . , x n )) was a variant of the coinductive tree generated by A(x 1 , . . . , x n ) in two key ways:

1. coinductive trees allow new variables to be introduced as one passes down the tree, e.g., with connected(x, y) ← edge(x, z), connected(z, y)

appearing directly in it, whereas, extending Example 6, p 1 (connected(x, y))

does not model such a clause directly, but rather substitutes terms on x and y for z, continuing inductively as one proceeds. 2. coinductive trees are finitely branching, as one expects in logic programming, whereas p(A(x 1 , . . . , x n )) could be infinitely branching, e.g., for GC with an additional unary operation s.

Modelling coinductive trees for arbitrary logic progams

We believe that our work in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF] provides an interesting model of ListNat, in particular because it agrees with the coinductive trees generated by ListNat. However, the account in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF] is less interesting when applied to GC, thus in the full generality of logic programming. Restriction to non-existential examples such as ListNat is common for implementational reasons [START_REF] Komendantskaya | Coalgebraic Logic Programming:from Semantics to Implementation[END_REF][START_REF] Johann | Structural Resolution for Logic Programming[END_REF][START_REF] Fu | A Type-Theoretic Approach to Resolution[END_REF][START_REF] Fu | Proof Relevant Corecursive Resolution[END_REF], so [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF] does allow the modeling of coinductive trees for a natural class of logic programs.

Here we seek to model coinductive trees for logic programs in general, a fortiori doing so for GC.

In order to model coinductive trees, it follows from Example 6 that the endofunctor Lax(L op Σ , P f P f ) on Lax(L op Σ , P oset) that sends At to P f P f At, needs to be refined as {{edge(x, z), connected(z, y)}} is not an element of P f P f At(2) as it involves three variables x, y and z. Motivated by that example, we refine our axiomatics in general so that the codomain of p n is a superset of P f P f At(m) for every m ≥ n. There are six injections of 2 into 3, inducing six inclusions At(2) ⊆ At(3), so six inclusions P f P f At(2) ⊆ P f P f At(3), and one only wants to count each element of P f P f At(2) once. So we refine P f P f At(n) to become (Σ m≥n P f P f At(m))/ ≡, where ≡ is generated by the injections i : n -→ m. This can be made precise in abstract category theoretic terms as follows.

For any Lawvere theory L, there is a canonical identity-on-objects functor from the category Inj of injections i : n -→ m of natural numbers into L op . So, in particular, there is a canonical identity on objects functor J : Inj -→ L op Σ , upon which Σ m≥n P f P f At(m)/ ≡ may be characterised as the colimit (see [START_REF] Lane | Categories for the Working Mathematician[END_REF] or, for the enriched version, [START_REF] Kelly | Basic concepts of enriched category theory[END_REF])

m∈n/Inj P f P f AtJ(m)
or equivalently, given n ∈ Inj, the colimit of the functor from n/Inj to P oset that sends an injection j : n -→ m to P f P f AtJ(m).

This construction extends to a functor P f f (At) : L op Σ -→ P oset by sending a map f : n -→ n in L Σ to the order-preserving function m∈n /Inj

P f P f AtJ(m) -→ m∈n/Inj P f P f AtJ(m)
determined by the fact that each m ∈ n /Inj is, up to coherent isomorphism, uniquely of the form n + k, allowing one to apply

P f P f At to the map f + k : n + k -→ n + k = m in L Σ .
This is similar to the behaviour of the monad for local state on maps [START_REF] Plotkin | Notions of computation determine monads[END_REF].

It is routine to generalise the construction from At to make it apply to an arbitrary functor H : L op Σ -→ P oset. In order to make the construction functorial, i.e., in order to make it respect maps α : H ⇒ K, we need to refine Lax(L op Σ , P oset) as the above colimit strictly respects injections, i.e., for any injection i : n -→ m, we want the diagram

Hn α n -Kn Hm Hi ? α m -Km Ki ?
to commute. Summarising this discussion yields the following: Definition 6. Let Lax Inj (L op Σ , P oset) denote the category with objects given by functors from L op Σ to P oset, maps given by lax transformations that strictly respect injections, and composition given pointwise. Proposition 2. cf [START_REF] Plotkin | Notions of computation determine monads[END_REF] Let J : Inj -→ L op Σ be the canonical inclusion. Define

P f f : Lax Inj (L op Σ , P oset) -→ Lax Inj (L op Σ , P oset) by (P f f (H))(n) =
m∈n/Inj P f P f HJ(m), with, for any map f : n -→ n in L Σ ,

(P f f (H))(f ) : m∈n /Inj P f P f HJ(m) -→ m∈n/Inj P f P f HJ(m)
determined by the fact that each m ∈ n /Inj is, up to coherent isomorphism, uniquely of the form n + k, allowing one to apply

P f P f H to the map f + k : n + k -→ n + k = m in L Σ .
Given α : H ⇒ K, define P f f (α)(n) by the fact that m ∈ n/Inj is uniquely of the form n + k, and using

α n+k : H(m) = H(n + k) -→ K(n + k) = K(m)
Then P f f is an endofunctor on Lax Inj (L op Σ , P oset).

The proof is routine but requires lengthy calculation involving colimits. Observe that we have not required countability anywhere in the definition of P f f , using only finiteness as we sought at the end of Section 4.

We can now model an arbitrary logic program by a map p : At -→ P f f At in Lax Inj (L op Σ , P oset), modelling ListNat as we did in Example 5 but now modelling the clauses of GC directly rather than using the awkward substitution instances of Example 6.

Example 7. Except for the restriction of Lax(L op Σ , P oset) to Lax Inj (L op Σ , P oset), ListNat is modelled in exactly the same way here as it was in Example 5, the reason being that no clause in ListNat has a variable in the tail that does not already appear in the head. We need only observe that, although p is not strictly natural in general, it does strictly respect injections. For example, if one views list(cons(x, 0)) as an element of At(2), its image under p 2 agrees with its image under p 1 .

Example 8. In contrast to Example 6, using P f f , we can emulate the construction of Examples 5 and 7 for ListNat to model GC.

Modulo possible renaming of variables, connected(x, y) is an element of At(2). The function p 2 sends it to the element {{edge(x, z), connected(z, y)}} of (P f f (At)) [START_REF] Benabou | Introduction to bicategories[END_REF]. This is possible by taking n = 2 and m = 3 in the formula for P f f (At) in Proposition 2. In contrast, {{edge(x, z), connected(z, y)}} is not an element of P f P f At(2), hence the failure of Example 6.

The behaviour of P f f (At) on maps ensures that the lax transformation p strictly respects injections. For example, if connected(x, y) is seen as an element of At(3), the additional variable is treated as a fresh variable w, so does not affect the image of connected(x, y) under p 3 . Theorem 3. The functor P f f : Lax Inj (L op Σ , P oset) -→ Lax Inj (L op Σ , P oset) induces a cofree comonad C(P f f ) on Lax Inj (L op Σ , P oset). Moreover, given a logic progam P qua P f f -coalgebra p : At -→ P f f (At), the corresponding C(P f f )coalgebra p : At -→ C(P f f )(At) sends an atom A(x 1 , . . . , x n ) ∈ At(n) to the coinductive tree for A(x 1 , . . . , x n ).

Proof. The construction of Theorem 1, subject to mild rephrasing, continues to work here. Specifically, (C(P f f )At)(n) is given by the same limit as in Theorem 1 but with At replaced by At(n) and with P f P f replaced by P f f : products in the category Lax Inj (L op Σ , P oset) are given pointwise, so the use of projections is the same; [Inj, P oset] is locally finitely presentable and P f f is an accessible functor, allowing us to extend the construction of the cofree comonad pointwise to [Inj, P oset]. It is routine, albeit tedious, to verify functoriality of C(P f f ) with respect to all maps and to verify the universal property. The construction of p is given pointwise, with it following from its coinductive construction that it yields the coinductive trees as required.

The lax naturality in respect to general maps f : m -→ n means that a substitution applied to an atom A(x 1 , . . . , x n ) ∈ At(n), i.e., application of the function At(f ) to A(x 1 , . . . , x n ), followed by application of p, i.e., taking the coinductive tree for the substituted atom, or application of the function (C(P f f )At)f ) to the coinductive tree for A(x 1 , . . . , x n ) potentially yield different trees: the former substitutes into A(x 1 , . . . , x n ), then takes its coinductive tree, while the latter applies a substitution to each node of the coinductive tree for A(x 1 , . . . , x n ), then prunes to remove redundant branches.

Example 9. Extending Example 8, consider connected(x, y) ∈ At(2). In expressing GC as a map p : At -→ P f f At in Example 8, we put p 2 (connected(x, y)) = {{edge(x, z), connected(z, y)}} Accordingly, p 2 (connected(x, y)) is the coinductive tree for connected(x, y), thus the infinite tree generated by repeated application of the same clause modulo renaming of variables.

If we substitute x for y in the coinductive tree, i.e., apply the function (C(P f f )At)(x, x) to it (see the definition of L Σ at the start of Section 4 and observe that (x, x) is a 2-tuple of terms generated trivially by the variable x), we obtain the same tree but with y systematically replaced by x. However, if we substitute x for y in connected(x, y), i.e., apply the function At(x, x) to it, we obtain connected(x, x) ∈ At(1), whose coinductive tree has additional branching as the first clause of GC, i.e., connected(x, x) ← may also be applied.

In contrast to this, we have strict naturality with respect to injections: for example, an injection i : 2 -→ 3 yields the function At(i) : At(2) -→ At(3) that, modulo renaming of variables, sends connected(x, y) ∈ At(2) to itself seen as an element of At(3), and the coinductive tree for connected(x, y) is accordingly also sent by (C(P f f )At)(i) to itself seen as an element of (C(P f f )At)(3).

Example 9 illustrates why, although the condition of strict naturality with respect to injections holds for P f f , it does not hold for Lax(L op Σ , P f P f ) in Example 6 as we did not model the clause connected(x, y) ← edge(x, z), connected(z, y) directly there, but rather modelled all substitution instances into all available variables.

Bonchi and Zanasi's approach to modelling logic programming in [START_REF] Bonchi | Saturated semantics for coalgebraic logic programming[END_REF] was to consider P f P f as we did in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF], sending At to P f P f At, but to ignore the inherent laxness, replacing Lax(L op Σ , P oset) by [ob(L Σ ), Set], where ob(L Σ ) is the set of objects of L Σ treated as a discrete category, i.e., as one with only identity maps.

The central mathematical fact that supports saturated semantics is that, regarding ob(L Σ ) as a discrete category, with inclusion functor

I : ob(L Σ ) -→ L Σ , the functor [I, Set] : [L op Σ , Set] -→ [ob(L Σ ) op
, Set] that sends a functor H : L op Σ -→ Set to the composite functor HI : ob(L Σ ) = ob(L Σ ) op -→ Set has a right adjoint. That adjoint is given by right Kan extension. It is primarily the fact of the existence of the right adjoint, rather than its characterisation as a right Kan extension, that enabled Bonchi and Zanasi's various constructions, in particular those of saturation and desaturation.

That allows us to mimic Bonchi and Zanasi's saturation semantics, but starting from Lax(L op Σ , P oset) rather than from [ob(L Σ ), Set]. We are keen to allow this as laxness is an inherent fact of the situation, as we have explained through the course of this paper. Such laxness has been valuable in related semantic endeavours, such as in Tony Hoare's pioneering work on the modelling of data refinement [START_REF] Jifeng | Categorical semantics for programming languages[END_REF][START_REF] Jifeng | Data refinement in a categorical setting[END_REF][START_REF] Kinoshita | Lax naturality through enrichment[END_REF], of which substitution in logic programming can be seen as an instance.

The argument, which was originally due to Ross Street, cf [START_REF] Street | The formal theory of monads[END_REF], goes as follows. where J : ob(L) -→ L is the inclusion, cf Bonchi and Zanasi's construction [START_REF] Bonchi | Saturated semantics for coalgebraic logic programming[END_REF], with its left adjoint, which is given by left Kan extension. The fact that the functor [J, P oset op ] also has a right adjoint, given by right Kan extension, implies that the monad T is finitary.

Corollary 2. For any Lawvere theory L, the inclusion With this result in hand, one can systematically work through Bonchi and Zanasi's paper, adapting their constructions for saturation and desaturation, without discarding the inherent laxness that logic programming, cf data refinement, possesses.

We have stated the results here for arbitrary lax transformations, but they apply equally to those that strictly respect injections, i.e., a subtle extension of the above argument shows that the inclusion [L op , P oset] -→ Lax Inj (L op , P oset) has a right adjoint, that right adjoint being a further variant of the right Kan extension that Bonchi and Zanasi used. The argument for lax naturality from the Introduction retains its force, so in Bonchi and Zanasi's sense, this does not yield compositionality of lax semantics, but it does further refine their analysis of saturation, eliminating more double counting.

Conclusions

For variable-free logic programs, in [START_REF] Komendantskaya | Coalgebraic semantics for parallel derivation strategies in logic programming[END_REF], we used the cofree comonad on P f P f to model the coinductive trees generated by a logic program. The notion of coinductive tree had not been isolated at the time of writing of [START_REF] Komendantskaya | Coalgebraic semantics for parallel derivation strategies in logic programming[END_REF], or of [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF], so we did not explicitly explain the relationship in [START_REF] Komendantskaya | Coalgebraic semantics for parallel derivation strategies in logic programming[END_REF], hence our doing so here, but the result was effectively in [START_REF] Komendantskaya | Coalgebraic semantics for parallel derivation strategies in logic programming[END_REF], just explained in somewhat different terms.

Using lax transformations, we extended the result in [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF], albeit again not stating it explicitly but again explained explicitly here, to arbitrary logic programs, including existential programs a leading example being GC, as studied extensively by Sterling and Shapiro [START_REF] Sterling | The art of Prolog[END_REF]. The problem of existential clauses is well-known in the literature on theorem proving and within communities that use term-rewriting, TM-resolution or their variants. In TRS [START_REF]Term Rewriting Systems[END_REF], existential variables are not allowed to appear in rewriting rules, and in type inference, the restriction to non-existential programs is common [START_REF] Jones | Type classes: An exploration of the design space[END_REF]. In LP, the problem of handling existential variables when constructing proofs with TM-resolution marks the boundary between the theorem-proving and problem-solving aspects, as explained in Section 2.

The papers [START_REF] Komendantskaya | Coalgebraic semantics for derivations in logic programming[END_REF][START_REF] Komendantskaya | Coalgebraic Logic Programming:from Semantics to Implementation[END_REF] also contained a kind of category theoretic semantics for existential logic programs such as GC, but that semantics was limited, not modelling the coinductive trees generated by TM-resolution for such logic programs. Here, we have refined lax semantics, refining Lax(L op Σ , P oset) to Lax Inj (L op Σ , P oset), thus insisting upon strict naturality for injections, and refining the construction P c P f At to P f f (At), thus allowing for additional variables in the tail of a clause in a logic program and not introducing countability, cf the modelling of local state in [START_REF] Plotkin | Notions of computation determine monads[END_REF]. This has allowed us to model coinductive trees for arbitrary logic programs.

We have further mildly refined Bonchi and Zanasi's saturation semantics for logic programming [START_REF] Bonchi | Saturated semantics for coalgebraic logic programming[END_REF], showing how it may be seen to complement rather than to replace lax semantics.

Definition 1 .

 1 Terms T er ::= V ar | F(T er, ..., T er) Atomic formulae (or atoms) At ::= P(T er, ..., T er) (Horn) clauses HC ::= At ← At, ..., At Logic programs P rog ::= HC, ..., HC

Example 3 .

 3 Let At consist of atoms A, B, C and D. Let P denote the logic program A ← B, C A ← B, D D ← A, C So p(A) = {{B, C}, {B, D}}, p(B) = p(C) = ∅, and p(D) = {{A, C}}.

Example 6 .

 6 Attempting to model Example 2 by mimicking the model of ListNat as a lax transformation of the form p : At -→ P f P f At in Example 5 fails. Consider the clause connected(x, y) ← edge(x, z), connected(z, y)

Theorem 4 . [ 3 ]

 43 For any finitary 2-monad T on a cocomplete 2-category K, the inclusion J : T -Alg s -→ T -Alg l of the category of strict T -algebras and strict maps of T -algebras into the category of strict T -algebras and lax maps of T -algebras has a left adjoint. Example 10. For any Lawvere theory L, there is a finitary locally ordered monad T on [ob(L), P oset op ] for which [L, P oset op ] is isomorphic to T -Alg s , with T -Alg l isomorphic to Lax(L, P oset op ). The monad T is given by the composite of the functor [J, P oset op ] : [L, P oset op ] -→ [ob(L), P oset op ]

  [L op , P oset] -→ Lax(L op , P oset) has a right adjoint.Proof. P oset is a complete 2-category as it is a complete locally ordered category. So P oset op is a cocomplete 2-category, and so [ob(L), P oset op ] is a cocomplete 2-category. So the conditions of Theorem 4 hold forExample 10, and so the inclusion [L, P oset op ] -→ Lax(L, P oset op ) has a left adjoint. But [L, P oset op ] op is canonically isomorphic to [L op , P oset], and Lax(L, P oset op ) op is canonically isomorphic to Lax(L op , P oset), and in general, a functor H : A -→ B has a right adjoint if and only if H : A op -→ B op has a left adjoint. The combination of these facts yields the result.

Ekaterina Komendantskaya would like to acknowledge the support of EPSRC Grant EP/K031864/1. John Power would like to acknowledge the support of EPSRC grant EP/K028243/1. No data was generated in the course of this research.


Philippe Ramirez
email: philippe.ramirez@cnrs.fr

Matrimonial patterns and trans-ethnic entities

Despite the complexity of their object of study, i.e. human society and culture, anthropologists seldom address complexity per se. In this paper I would like to briefly suggest approaches to deal with certain complex issues involved in the modelisation of social relations within a naturalistic paradigm. What I want to show primarily is how anthropological knowledge might be markedly enhanced by truly confronting the complexity of anthropological phenomena, i.e. by putting culture and social structures back into the natural/physical world, to understand how "it really works". And the condition for performing such an enterprise is close cooperation with other disciplines dealing with the study of complexity. The topic at hand is modelling the origin of a system of surname equivalences in tribal India. But the work being done might have a much broader range, by helping the studies of matrimonial systems to adopt more naturalistic approaches.

Georg Simmel wrote about "large systems", formed of "immediate interactions that occur among men constantly…that have become crystalized…attaining their own laws" (Simmel 1950, 10). The present study aims at understanding how one of these systems evolves "by itself", beside or in conjunction with what the actors say and think about it.

Among several tribal societies of North-East India people recognize that some of their neighbours, belonging to altogether different cultures and ethnicities, and speaking different languages, are actually "similar" because of their surname. "Similar" people are identified by their surnames being "the same". We might translate without too much risk "similar" by "synonymous" or "equivalent", as such surnames refer to clans ("descent groups" in the anthropological parlance), the immediate outcome being that equivalent clans are found across different ethnicities. "Similar" people from different tribes are not bound to any mutual obligation other than the absolute ban of intermarriage: being the same they should not marry, which would amount to an incest, the worst crime in those societies. Thus, being different in terms of ethnicity and culture does not preclude being the same in terms of clan, which is a counter-intuitive idea for many anthropologists and for many North-East Indians as well, especially those belonging to the younger generations. Anthropologists have been taught in universities that tribal societies consist of clans who share a common culture and a common social structure. And young North-Easterners are immersed in a neo-essentialist, ethnicized India where different people are different by all means: how could they be both different and similar?

The initial question which the research described here tries to address is the origin of such a system, with the view that in the absence of a centralized authority such relations may have been the product of processes of self-structuration. Systems displaying similar features (clanic equivalence implying exogamy) have been documented in other areas of the world, although they are globally rare: Western Siberia, North America, North-East Africa (Swanton 1909;Verbov 1936;[START_REF] Goodwin | The Characteristics and Function of Clan in a Southern Athapascan Culture[END_REF][START_REF] Emmons | The Tlingit Indians[END_REF][START_REF] Shternberg | The Social Organization of the Gilyak[END_REF]. Very few systematic studies have been undertaken on the topic, with the exception of Robinne, on the Kachin of Upper Myanmar (Robinne 2007), and Günther Schlee in the Horn of Africa (Schlee 1985). Schlee suggested that the origin of equivalences among ethnically different -but linguistically related-people was a series of segmentation processes dividing original clans into branches with different titles, but who still remembered being related. This scenario cannot hold for the North-East India case, which involves culturally unrelated people who arrived on the scene at various times and from different directions.

My data pertains to three particular ethno-cultural entities, to three "tribes" (tribe being the established term in local English): the Tiwa, Karbi and Khasi, and more particularly to the 2.500 km² or so of low hills on the Meghalaya and Assam states borders where the villages of these tribes are interwoven, each village being monoethnic. The differences among these three tribes are obvious. They speak very dissimilar languages, which either belong to different branches of the Tibeto-Burman family (Karbi, Tiwa) or to the Austroasiatic family (Khasi). The Karbi follow patrilineal descent: clan membership and surnames are inherited on the male line. Khasi follow matrilineal descent. And among the Tiwa, descent is ambilineal: according to where the new couple decides to reside, their children will inherit either their mother's or their father's clan and surname. Social and political structures as well as traditional religions (between 30% and 60% are Christians) are less contrasted, but enough to form three (relatively) different cultures. Finally, in the domain of identity, ethnicities are neatly asserted -which may not have been the case in the past. People have no doubt they belong to one particular tribe and that this tribe has "nothing to do" with the next one.

To fully complete this rough picture of the context, two points have to be added. First, before a sharp population growth during the twentieth century, which led to sedentarization, short distance migrations, driven mostly by slash-and-burn agriculture as well as epidemics, were pervasive. Second, inter-ethnic marriages were less than marginal and are now on the rise. Their precise amount is difficult to assess, as the incoming spouses fully adopt the local culture, and even change their surname, actually on the basis of the interethnic surname equivalences. And in interethnic marriages, exogamy between equivalent surnames is, up to my data, strictly respected.

Most elderly persons know about the existence of surname equivalences. In a particular locality, or family, people cannot list the full equivalence relations linking all the clans; they would only cite a few of them; similarly, they most generally cite one to one equivalences relations between one clan of their own tribe and one of the two other tribes. Strikingly however, when put together, the collected equivalences fully agree and draw a very coherent picture (Figure 1, below). The lines in the diagram should be read as "Surname A is equivalent to surname B", or "people bearing surname A cannot marry people bearing surname B". The diagram includes exogamic relations internal to each tribe, i.e. the clans within each tribe who are forbidden to marry, each cluster forming what anthropologists call a "phratry". One notices the striking correspondence between "internal exogamies" and "external" ones, particularly between the Karbi and Tiwa. Among these two tribes at least, exogamy is transitive across the ethnic boundaries: e() being the relation of exogamy, Tn a Tiwa clan and Kn a Karbi clan, (Ta e(Ka)) ^ (Ka e(Kb)) ⟹Ta e(Kb).

Where did such a coherent system come from? The possibility that, as in the Horn of Africa, equivalences are the links which remained after original descent groups split up, can be discarded, as the tribes concerned differ in all aspects. Intentional creation also comes to mind as a possible origin. However, we're among tribal societies, with no overarching centralized authority. We have no signs that the neighbouring Hindu rajas, with whom the tribes had at different times maintained loose alliances, have interfered with their marriage rules -and this seems hardly plausible anyhow. The highest level authorities which could have regulated marriages are the politico-ritual dignitaries responsible for the settlement of disputes and the performance of rituals, but their authority seldom stretched beyond a dozen villages. And even in this case, what would have been the reason for coordinating interethnic marriages?

To me, the most plausible scenario to account for the origin of equivalences is that of selforganization and diffusion. Equivalences would have emerged locally in the context of interethnic marriages, when different matrimonial norms were confronted. They then would have diffused to other localities and/or connected with similar patterns. Presently, among the Khasi and Tiwa, there exist no other matrimonial rule than clan exogamy. On the Karbi side however, informants describe their traditional but vanished ideal rule as a circulative connubium, i.e. cyclical marriages among their five major clans (A->B->C->D->E->A).1 Nowadays, the only norm among the Karbi is the avoidance of symmetrical alliances between local lineages, and this is largely adhered to: after a local lineage (i.e. segment of clan) belonging to clan A have "taken a girl" from a lineage belonging to clan B, upcoming marriages between the two lineages will only be allowed in the same direction; B will not "take a girl" from A and the orientation of the relation will not be allowed to reverse for several generations. Any marriage thus creates an asymmetrical relation between "wife-givers" (WG) and "wife-takers" (WT), all men born in the WG lineage being afterwards addressed by their WT as ong, indistinctly meaning "father-in-law" and "maternal uncle". Thus, when Karbis consider a new matrimonial alliance, they must ensure that existing WG-WT relations will not be jeopardized.

My hypothesis is the following: after a Karbi marries a member of another tribe, a WG-WT is established between the partner lineages. The foreign lineage becomes structurally equivalent to a Karbi lineage and becomes identified with a Karbi surname. This will be taken into consideration in future marriages. After several such interethnic marriages happen in the neighbourhood, a full set of equivalences becomes established between the Karbi clans and the non-Karbi clans. This set of equivalences then spreads to the neighbouring localities. An alternative, more plausible and more complex scenario, is that different sets of equivalences were born in several distant localities and that after a while they coalesced into a unified regional system.

The question is: how much time would it take for such a scenario to be completed in a particular population/area? The core of this scenario can be qualified as a weak emergence. It is extremely simple to simulate for ideal conditions and a single locality: each new marriage generates a new WG-WT relation and forbids its reversal. After n interethnic marriages have taken place between n distinct Karbi clans and n distinct non-Karbi clans, n equivalences are established. This could be a matter of two generations only.

Modelling the same process in a moderately realistic way would however involve a lot of factors, making us enter the realm of complexity (both computational complexity and complex dynamic systems). First, in the real world, there is little chance that three interethnic marriages involving 2x3 distinct clans will happen in a row within one or two generations. The communities involved are villages of a few dozen houses, thus the frequency of matrimonial unions are limited. Considering the time factor brings to the probability that a marriage between two particular lineages takes place, and first of all that it is contemplated by the families. A prospective marriage corresponds to two households situations matching, possibly to the agreement or feelings of the prospective spouses, and to the mere existence of matchable individuals, i.e. at least the availability of a bachelor of the right age: the local population's structure is a critical factor. Furthermore, the probability that a member of a particular clan marries a member of another particular clan depends on the availability of these two clans in the surroundings. Now, considering the small populations at stake, this situation is not obvious. Second, a simulation of the build-up of equivalences in a local isolate does not take into account what occurs outside. Now what would happen if a similar process happens in the next area? There is little chance that the very same equivalence relations will emerge. So, how will contradictions between two sets of equivalence be resolved if a marriage is considered between people living in both areas?

These rather mechanistic issues don't bother most anthropologists. When describing social structures and norms, anthropologists seldom consider their applicability in a realistic context. I believe that the question of the origin of equivalences cannot be settled in a useful manner by considering the social structure and the norms supposed to regulate it in isolation from their biological environment. What would be the point of showing that the asymmetrical marriage rule might generate surname equivalences if there is very little chance that the proper matrimonial configuration appears over several centuries? This is the reason why I decided to solicit the expertise of statisticians, modellers and ecologists, among others, and set up a working group, ATIMODIS, to decipher the processes at stake in the complex relations between marriage rules, space and population dynamics.

For the time being, ATIMODIS has tried to identify which factors might be critical in the modelling of the hypothesis in question. To start with, a series of simple simulations (under GAMA 2 ) involving only a small population and a simple set of marriage rules have helped to put into light a very critical factor indeed: the fragility of small populations to even seemingly light marriage constraints. Imposing nothing more than the simple rule of clan exogamy ("one should not marry within one own's clan") to a population of 200 individuals divided into three clans, even with optimistic fertility rates, will considerably endanger its survival in less than three centuries. Going a step further by imposing an asymmetrical marriage rule among the clans ("after A has taken from B, it will not be able to give back") will make the population dramatically collapse and disappear within less than three to four generations. As for the circulating connubium, with three clans exchanging, even when a degree of deviance is allowed for, eligible partners become unavailable after a couple of years, preventing any reproduction. Although the "small population effect" or "demographic stochasticity" is nothing new 3 , realizing how much any pairing constraint amplified its consequences forced us to somehow let the question of equivalence aside for a while, and focus on the relationships between matrimonial rules and population viability. In which conditions could the prescriptive marriage norms formulated by the Karbi have been applied at all? Our simulations showed that the ideal norm of the circulating connubium, what anthropologists after Lévi-Strauss call the "generalized exchange", with three or five clans exchanging spouses in a single direction, seems impossible to put into practice in a small population when a majority follows the rule. This incited me to go back to the anthropological literature on generalized exchange. Lévi-Strauss himself had noticed that the structural model he proposed was hardly applicable in practice, both because of population size effects (on which he did not elaborate much) and because of the inequalities among the exchanging parties (Lévi-Strauss 1969, chap. introduction). Indeed, Leach and others had criticized him on the ground that nowhere was generalized exchange statistically dominant (Leach 1962). Lévi-Strauss reacted by arguing that generalized exchange is primarily a "model": its "reality" (accuracy) does not consist in its statistical existence but in the fact that it depicts the general trend of all concrete alliances in the long term. As a matter of fact, some scholars, with the limited tools of the time (1960s-1970s), had started to show through simulation both that the rule was impossible to put fully into practice and conversely that in the absence of any other rule than simple exogamy, there was always a proportion of marriages corresponding to the norm of generalized exchange [START_REF] Kunstadter | Demographic Variability and Preferential Marriage Patterns[END_REF][START_REF] Gilbert | Computer Simulation and Analysis of Problems in Kinship and Social Structure[END_REF]. If other aspects of the generalized exchange model still arouse new formalizations and modelizations (e.g. graphs4 ), the study of its demographical context have not benefited from the computational and simulation tools now at our disposal. This is one of the tasks ATIMODIS project wishes to take on.

Although generalized exchange in its full cyclic form has not been documented, cases of populations following prescriptive asymmetrical rules are widespread [START_REF] Leach | The Structural Implications of Matrilateral Cross-Cousin Marriage[END_REF][START_REF] Moore | Oblique and Asymmetrical Cross-Cousin Marriage and Crow-Omaha Terminology[END_REF][START_REF] Löffler | Prescriptive Matrilateral Cross-Cousin Marriage in Asymmetric Alliance Systems: A Fallacy[END_REF][START_REF] Krige | Asymmetrical Matrilateral Cross-Cousin Marriage-the Lovedu Case[END_REF]. If simulations show that asymmetrical rule is so detrimental to the demographic structure, how then could it be explained that populations practising such marriages were able to survive? The issue was seldom taken up by anthropologists. Recently however, starting from this very question, a set of studies in Western Australia have brought a very convincing and stimulating answer, and one which compel us to deeply reconsider our methodology, if not our paradigm: a few exchange of partners among local groups could have been sufficient to maintain their demographic viability even while prescriptive alliance remained dominant [START_REF] Dousset | Assimilating Identities: Social Networks and the Diffusion of Sections[END_REF][START_REF] White | The Indigenous Australian Marriage Paradox: Small-World Dynamics on a Continental Scale[END_REF][START_REF] Denham | Beyond Fictions of Closure in Australian Aboriginal Kinship[END_REF]. Small populations are very rarely complete isolates. Their sustainability cannot be explained without taking into account the inputs from outside, even if these look statistically marginal. Statistically marginal exogamy may prove vital for the survival of small populations.5 "Intermarriage … should be seen as a component of formal marriage system models that opens up local models to form an explicit, culturally recognized, and realistic continentwide meta-model." (White and Denham 2007, 6) Thus the need to move from the level of the village, where most marriages happen, to the regional level, at which inter-villages marriages take place from time to time, in order to understand how the two levels are dynamically connected. In other words, shifting from the (false) local isolate to what ecologists call the meta-population. In this regard, the contribution of the tools used by ecological modelling could be essential for the approach of anthropological complexities such as the interactions between marriage norms and demographics.

The "problem" posed by the negative effects of marriage rules on the demographic dynamics of small populations could in fact be completely reversed. In a functionalist perspective, and at least as a working hypothesis, one could consider prescriptive marriage rules not as a constraint but as an incentive to search for mates outside the group -whatever group -which would counter demographic stochasticity as well as genetic inbreeding.

Modelling the dynamics of asymmetrical marriage rules at the level of meta-populations is however far from being a trivial task. This is where one enters into hardcore complexity (at least to an anthropologist) and where interdisciplinary becomes compulsory. For instance, how did different local matrimonial patterns become a coherent regional pattern? Simulation will obviously be a major component of our approach. The second one will consist in mapping the data available on existing matrimonial links. A set of genealogies I collected in some localities will help to understand the small-scale mechanisms, but hardly any phenomenon of emergence/selforganization. For this purpose, our main corpus will be the Indian electoral rolls, which provide a full size picture of voters with their surnames, including married women and their husband names, and thus of the existing alliances among clans. This set of data has several obvious limitations, among others the inability to show the origin of external spouses, or to show real matrimonial networks. The challenge will be here to devise proper tools that will explore the corpus at successive spatial levels and detect the existence of significant patterns.

For the time being, it is interesting to underline how a very pragmatic problem emerging during simulation, "how to avoid that my population collapses", has led to a deep re-thinking of the general approach. Going back to the literature about the anthropological theory of alliance, I realized that the problem had not been resolved at all, and that other essential issues as the structuration of alliance patterns at higher levels remained almost untouched. An approach in terms of complexity is not an escape out of the classical anthropological debates; indeed it is a constructive return to them.

Figure 1

 1 Figure 1 Endo-ethnic and interethnic exogamies among Karbis, Tiwas, and Khasi-Bhois of Assam-Meghalaya borderlands. Dots represent patronymic groups (clans), lines represent relations of exogamy. This diagram highlights the convergence of exogamies within ethnic groups (same color clusters) and across them.

On similar norms, see e.g.[START_REF] Needham | Circulating Connubium in Eastern Sumba: A Literary Analysis[END_REF][START_REF] Lehman | The Structure of Chin Society[END_REF]

https://github.com/gama-platform/gama/wiki

See for instance[START_REF] Dyke | Potential Mates in a Small Human Population[END_REF][START_REF] Gaines | Simulating Success or Failure: Another Look at Small-Population Dynamics[END_REF][START_REF] Legendre | Demographic Stochasticity and Social Mating System in the Process of Extinction of Small Populations: The Case of Passerines Introduced to New Zealand[END_REF][START_REF] Engen | Demographic Stochasticity and Allee Effects in Populations with Two Sexes[END_REF][START_REF] Drake | Allee Effects | Learn Science at Scitable[END_REF]). For human populations, a "Minimum Viable Population" of 500 has been suggested by[START_REF] Livi | Considérations Théoriques et Pratiques Sur Le Concept de 'Minimum de Population[END_REF]).

[START_REF] Harary | The Logical Structure of Asymmetric Marriage[END_REF]

This converges with conclusions met by paleo-anthropologists. (Bocquet-Appel and Masset 1982).