Yannick Chevalier
email: yannick.chevalier@irit.fr

Theory Synthesis based on Experience

Keywords: Algebraic domains, Geometric Logic, Knowledge Representation, Learning Algebraic domains, Geometric Logic, Knowledge Representation, Learning Rapport technique

We present in this paper a novel approach to learning that produces practical and conceptual knowledge. The former aims at detecting changes or new behaviour in observations, a trait of anomaly detection systems, and that practical knowledge can be updated based on an Angluin-like property. The second one aims at enabling communication with an expert user by producing a first-order logic model of the world observed.

This construction fills the gap in previous work by Achourioti and van Lanbalgem were inverse systems of first-order logic models are employed to formalize Kant's transcendental logic.

More precisely learning is modeled by algebraic morphisms on algebraic lattices. Composition of morphisms is denoted by first-order terms interpreted as intensional tables or constraints on tables. Data Exchange Systems (DXS) are set of terms describing databases storing information about observations and observed constraints. Practical knowledge is a valuation of a DXS and the associated skill is to decide whether a new event is conform to past events, a new behaviour or an anomaly. When the decision is wrong, the DXS is updated according to whether an anomaly or a new normal behaviour was wrongly assessed.

These DXS are enriched with sets of terms representing tables of interest or generic constraint, resulting in cognitive states. A first-order model is constructed for each compact cognitive state and contains the set of predicates that are sensible given the observations and the cognitive state. We finally prove that these models form an inverse system of models whose limit is the starting point of the formalisation of Kant's Transcendental Logic.

Introduction

Background and motivations. Learning and knowledge are introduced along seemingly independent approaches. In a symbolic setting, learning was first defined [START_REF] Gold | Complexity of automaton identification from given data[END_REF] as improving a procedure guessing the membership of a word in a regular language. Angluin's theory [START_REF] Angluin | Learning Regular Sets from Queries and Counterexamples[END_REF] focus on learning the language given membership examples and counter-examples. PAC learning [START_REF] Valiant | A Theory of the Learnable[END_REF] generalised further the problem by assuming a probability of failing to learn, and when succeeding in learning a possibility of error in answering queries.

The definition of practical knowledge in this paper stems from the need to formalise an absence of knowledge, e.g., when analysing pseudo-random sequences. These are defined in [START_REF] Andrew | The Complexity of Pattern Matching for a Random String[END_REF] as sequences such no Turing Machine is able to compute in polynomial time a meaningful prediction of the next bit given a sequence of bits already produced. This approach is extended in computational cryptography where having zero knowledge about an object represented with a string s is modeled as having no couple of Turing Machine (TM) such that the second one is able to determine whether the first one had s or a random string on its input tape [START_REF] Feige | Zero Knowledge Proofs of Identity[END_REF]. To introduce the vocabulary of this paper, an object is formed by the first TM, and the second TM computes a representation. Absence of knowledge is defined as the inability to compute any meaning representation. As a contrapositive, knowing something is being able to compute a meaningful representation.

More recently and more directly related to this paper it was proven [START_REF] Bana | A Computationally Complete Symbolic Attacker for Equivalence Properties[END_REF] that symbolic first-order logic techniques can be employed to model and decide computational cryptography lack of knowledge by static equivalence [START_REF] Abadi | Deciding Knowledge in Security Protocols Under Equational Theories[END_REF]. In this symbolic setting, agents' knowledge about a term describing a sequence of messages is specified by a set of equations satisfied only by possible instances of these messages. Under some additional hypotheses it is possible [START_REF] Chevalier | Compiling and Securing Cryptographic Protocols[END_REF] to compute from a generic term a set of tests that entirely determines membership in the set.

Finally formal concept analysis (FCA) [START_REF] Davey | Introduction to Lattices and Order, Second Edition[END_REF][START_REF] Wille | Restructuring Lattice Theory: An Approach Based on Hierarchies of Concepts[END_REF] embeds objects and attributes into a lattice to form concepts of similar objects with respect to their attributes. The partial grouping of objects per similarity can be modeled with a partial equivalence relation that naturally leads to algebraic lattices [START_REF] Bauer | Equilogical spaces[END_REF]. Conceptual knowledge is the extension of concepts to predicates of arbitrary arity, while classes of indistinguishable object terms (according to the predicates at hand) form a domain on which these predicates are interpreted.

Approach. In response to Empiricists such as Hume, Kant provided an answer to the problem of causation based on the analysis of human thought process [START_REF] Kant | Critique of the Pure Reason ; Translated from the German by Paul Guyer and Allen W. Wood[END_REF]. Though Frege's formalisation of first-order logic [START_REF] Frege | Begriffsschrift: Eine der Arithmetischen Nachgebildete Formelsprache des Reinen Denkens[END_REF] seemed to enlighten Kant's formalism, it was objected in [START_REF] Longuenesse | Kant and the Capacity to Judge: Sensibility and Discursivity in the Transcendental Analytic of the Critique of Pure Reason[END_REF] that this formalisation over-simplified Kant's work by reducing the act of the mind called cognition to deduction, a mere syntactic manipulation. More recently, inverse systems of first-order logic models were proposed [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF] as a basis to formalise Kant's analysis. A difficulty in any tentative formalisation is that according to Kant logic is based on cognitions, that these cognitions define a semantics, and that this semantics determines the syntax, a departure from more modern descriptions of logic.

Beyond philosophy and metaphysical considerations, puzzling out Kant's analysis is interesting to the modern computer scientist as it promises a natural description of observations under the guidance of primitive categories which in addition to causality encompass temporality and space. This approach is highly relevant e.g., in anomaly detection in which a usable system must be able to describe suspicious behaviour to network experts in a high-level language [START_REF] Sommer | Outside the Closed World: On Using Machine Learning for Network Intrusion Detection[END_REF]. This paper extends the proposal in [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF] as follows. Cognitions are defined as algebraic morphisms between algebraic lattices. Their compositions is denoted with first-order terms whose interpretation in algebraic lattices is updated to fit observations. A single comparison predicate is added to create an observation model. These terms are separated into object and representation terms. Two subsets of presentation and object terms considered for further examination determine respectively a set of predicates as conjunction over the observation model and a domain as a set of partial equivalence classes of object terms wrt these predicates. We prove these models form an inverse system of models.

Limitations. The construction presented in this paper coincides with the one in [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF] when the observation of the world is fixed. This can be explained by the focus in [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF] on the construction of a model in which the cognitions and the logic can be characterised as geometric logic [START_REF] Vickers | Continuity and Geometric Logic[END_REF] . There are differences in our construction wrt Kant's model of cognition as presented in [START_REF] Longuenesse | Kant and the Capacity to Judge: Sensibility and Discursivity in the Transcendental Analytic of the Critique of Pure Reason[END_REF]: the choice of remembering past observations rather than reconstructing them, and the lack of focus on the temporal relation between events.

Organisation. The choice of algebraic lattices and morphisms to denote respectively knowledge and learning is justified in Section Section 2, and the corresponding aLAT ! category is introduced with its salient properties. The learning process is defined in Section Section 3. The target of this first learning process is practical knowledge, introduced together with a limited formalisation of skills in Section Section 4. It is proved that the skill can be improved through learning, an Angluin-like property. Section Section 5 introduces cognitive states and Conceptual knowledge as first-order models on compact cognitive states before being extended to all stable cognitive states in Section Section 6.

Future works are presented in Section Section 7.

Modeling Learning

Informal considerations

Per the Oxford dictionary, learning is the acquisition of knowledge or skills through study, experience, or being taught.

Without going into the definitions of knowledge and skills it can be infered that they increase through the three stated activities. Let d, d be datasets representing observations of the world, and assume that d ⊆ d . Then a learning algorithm f applied on d should return a better result than when applied on d, something we denote with f (d) f (d ). We infer from this comparison that both the input and output of the function must be posets and that f must be a monotonic between these posets. Reasoning along the same lines, we conclude that any learning function must be monotonic wrt studying (cognitions) and being taught (user-given information).

Independently, Kant defines logic as the rules of discurse that enable the construction of truth from observations. A central tenet in his analysis is the always present possibility of reconciling different positions as long as they were established through the proper rules. This reconciliation process is presented in [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF] through the unity of self that must be preserved during the establishment of any proper theory of the world. Mathematically speaking, if both d, d are datasets representing different observations of the world and f is a learning algorithm, denoting the amalgamation of the experiences and of their results we have

f (d d ) = f (d) f (d ).
This implies inter-alia that the codomain of f is a joinsemilattice. It is then natural to also assume that if d ⊥ represents the minimum experience, then f (d ⊥ ) should also be the minimum value in the codomain of f . Another postulate is that the theories properly constructed from experience should converge towards an ideal description of the world. It was already noted in [START_REF] Abramsky | Domain Theory in Logical Form[END_REF] that this postulate implies the existence of a Stone duality [START_REF] Mark | 1. Classical Stone Duality[END_REF] theorem between the world as a model and the theory constructed. To construct a meaningful theory one has to assume that the observed world is not random and thus that not all sequences of events are possible. Thus the possible observations of the world are bounded by a set d of possible sequences. Then for all sequences of sets of observations (d n ) n∈N that converges towards d, i.e., such that ∪ n∈N d n = d, we should also have n∈N f (d n ) = f (d), even if the latter can only be asserted to exist and not computed explicitely. This implies that the limits ∪ n∈N d n and

n∈N f (d n ) exist if (d n ) n∈N
is an increasing sequence of observations. Since both the domain and codomains are lattices, this implies that they are actually complete lattices, and that f is Scott-continuous.

Model for machine learning

We now present the formal setting, with well-known referencing definitions and properties in [START_REF] Abramsky | Domain Theory[END_REF].

Definitions. Let (P, ) be a poset. Given x ∈ P we denote ↓ x = {y ∈ P | y x)}. A subset X ⊆ P is an ideal whenever x ∈ X and y

x imply y ∈ X. The set of ideals of P ordered by inclusion is denoted Idl(P ). It is well-known that since P is a poset, Idl(P ) is a complete lattice: the infimum and supremum all subsets of X ⊆ Idl(P ) are defined, and denoted respectively X and X.

An element x ∈ Idl(P ) is compact whenever for all sets X, x X implies there exists a finite Y ⊆ X such that x Y . Since Idl(P ) is a complete lattice it is bounded complete: if x, y z then x y z. A subset X of P is directed whenever for all x, y ∈ X, there exists z ∈ X such that x z and y z. It is wellknown that since P is a poset, the compact elements K(Idl(P )) of Idl(P ) are (up to isomorphism) the elements of P . Given x ∈ Idl(P ) denote x ↓= K(Idl(P ))∩ ↓ x. It is well-known that this set is directed, and that x = x ↓ for all x ∈ Idl(P ): K(Idl(P )) is a base of Idl(P ), thus Idl(P ) is an algebraic lattice.

Traces, Observations, and Object Domains. Let A be an alphabet of events. A trace is a word in A * . During the learning phase, a set of traces L is availabe for learning. For u, v ∈ A * denoting u v if u is a prefix of v, we note that whenever v is observed and u v then u also is observed. Thus the set of effectively observed traces in the course of learning is ↓ L, that is the ideal defined by L, from now on called an observation. Since (A * , ) is a poset, Idl(A * ) is an algebraic lattice. The compact ideals of Idl(A * ) are generated by finite subsets of A * . We denote a compact ideal I with Σ n i=1 u i if {u 1 , . . . , u n } is the intersection of all subsets S ⊆ A * such that ↓ S = I. Given an alphabet A Idl(A * ) is denoted T A and called the object domain of A.

The aLAT ! category. We consider in this paper domains which are algebraic lattices. It is well-known they are always complete. The bottom (resp. top) of a domain A is ∅ = ⊥ A (resp. ∅ = A ). We consider morphisms between domains that are:

• Continuous: f ( X) = x∈X f (x) for every X ⊆ A); • Strict: If f : A → B, then f (⊥ A ) = ⊥ B .
A domain morphism mapping compact elements to compact elements is algebraic. A learning function is an algebraic morphism. The objects of the aLAT ! category are the domains and its morphisms are the strict continuous morphisms.

Example 1. Any finite lattice is a domain. Thus for example the usual boolean lattice B = {0, 1} with 1 0 is a domain. The Belnap four-valued lattice [23] {U, T, F, C} (unknown, true, false, contradictory) with U T, F and T, F C is also a domain. More generally any finite lattice, including concept lattice [START_REF] Wille | Restructuring Lattice Theory: An Approach Based on Hierarchies of Concepts[END_REF] employed to classify data hierarchically, is a domain. Another generalisation of Belnap's four-valued lattice is to consider any unordered set S and equip it with a top and a bottom element. The resulting ordered set S ∪ { , ⊥} is a domain. Finally the set of subsets of N equiped with the union operation and the inclusion ordering is a domain whose compact elements are the finite subsets of N.

Example 2. Let D spr be the domain R + ∪ {+∞} equiped with x y = min(x, y). The minimum of that domain is +∞ and its top element is 0. The minimum is the only compact element. Equiped with D spr it is possible to memorize the record time in a sequence of sprint races.

Lifting. It is convenient to define functions the alphabet A, or at least on finite words. Such definitions, provided the codomain is a domain, can be canonically extended into a morphism.

Definition 1.

Let A be an alphabet, D be a domain, and f : A * → D be such that for all u, v ∈ A * , u v implies f (u) f (v). The lifting of f is denoted f : T A → D and is defined by:

f (u) = v∈↓u v = Σ w∈B w w ∈ B f (w)
The definition of hatf ensures that all limits commute with its application.

Proposition 1.

Let A be an alphabet, D be a domain, and f : A * → D be such that for all u, v ∈ A * , u v implies f (u) f (v). Then f ∈ [T A → D] is also algebraic.

Properties of the aLAT ! category

It is well-known that the aLAT ! category is cartesian closed. [START_REF] Davey | Introduction to Lattices and Order, Second Edition[END_REF] In particular its exponential is an algebraic lattice. The support of a function f :

D → E is the minimal subset S ⊆ D such that x / ∈ S implies f (x) = ⊥ E . It is well-known that the compact elements of [D → E] are the functions with a finite support S such that f (x) is compact for all x ∈ S. Proposition 2. If D, E are objects in aLAT ! then [D → E] also in aLAT ! .
Proof. By Prop. 4.1.5 of [START_REF] Abramsky | Domain Theory in Logical Form[END_REF]: algebraic lattices are continuous lattices.

Example 3. In particular a database table whose elements are in a domain and indexed by keys in a domain can be encoded as a function between these domains. To be admissible, the construction of a database must be an algebraic morphism and thus map observations to finite tables.

In particular we use without further reference that the product n∈N D n is in

Split functions

Observations are analysed in a loop involving first the discovery of properties of events, then the classification of events according to these properties. This classification yields a denumerable set of classes that can be analysed independently. This possibility of finer-grained analysis justifies the introduction of specific classification morphisms, the split functions. Example 4. Continuing the sprint example, it is natural to classify the humans running according to their speed, e.g., define athlete as someone able to run in less than 12s. This classification should be complete, i.e., encompass all the events seen so far. It is also arbitrary, in the sense that assuming an object domain T S , a choice function c is just any function S → N. The split function for c maps each event e to the c(e)th copy of S. It is denoted Split c and maps an object u ∈ T S to an element Split c (u) = (u n ) n∈N ∈ n∈N T S . The notation (u n ) n∈N is defined on events and the Split c function is lifted to elements of T S with Prop. 1. Proposition 3. Let T S be an object domain, and c be a choice function on S. Then Split c is algebraic.

Proof. First since aLAT ! is cartesian closed n∈N T S is in aLAT ! . The Split c morphism is by construction strict and continuous, we have to prove it is algebraic. The compact elements of its codomain are the sequences of finite support such that all the values are compact. Let u = (u n ) n∈N ∈ n∈N T S = Split c (v). If v is compact then it is an observation, a finite set of traces, and thus there is only a finite number of events occuring in v. Each event has one class, thus Split c (v) is of finite support. For all n ∈ N the value u n is an observation and thus is compact. Thus if v is compact then Split c (v) is compact.

Example 5. The domain D spr of Ex. 2 is a representation domain. A function that extracts from each event its runner and run time can be lifted into an algebraic morphism mapping an observation u to another observation u . One can compute a representation of u -and therefore of u-with a table associating to persons their record time. A representation containing the minimum value in that table can then be computed. A piece of knowledge that can be extracted from this representation of the observation u is that all humans run 100m in at least that minimum value.

Learning

Given our primary interest on anomaly detection systems we borrow from [START_REF] Chevalier | Data Exchange for Anomaly Detection: The Case of the CAN Bus[END_REF] the naming conventions on filters and Data Exchange Systems. Summarily this work on the resolution of simple Data Exchange (DX) problems to fill tables in a database and on filters (to be understood as filters in dynamical system analysis, not as the topological construction) to learn integrity contraints. This generalisation follows the approach to DX of [START_REF] Spivak | On The Relational Foundations Of Functorial Data Migration[END_REF] in which rules are modeled as morphisms between objects that represent tables. In contrast with that work we are not interested in learning complex diagrams, and focus on the values computed in acyclic diagrams with one source. Accordingly a database is modeled with a set of terms, each term denoting either the composition of functions filling a table (an object term) or a filter (a representation term).

Notations

We let D 0 , D 1 , . . . , D n be objects in aLAT ! . The domain D 0 plays the particular role of being an object domain which is the source of the observations. Some of these are object domains, the other are called representation domains. We consider a set F of algebraic morphisms f 1 , . . . , f m between these domains, with f ∈ F of arity k f and:

f : D α f (1) × • • • × D α f (k f ) → D α f (0)
for a mapping α f : {0, . . . , k f } → {0, . . . , n}. We also let S be a set of n s split functions Split ci 1≤i≤ns over objects domains D αc i for α ci ∈ {1, . . . , n}. A function is a representation whenever its codomain is a representation domain, and an object function otherwise.

First-order signature. A sort τ i is associated with each domain D i , for 0 ≤ i ≤ n. The sorted first-order functional signature Σ F,S comprises 1. The set of function symbols f 1 , . . . , f m with sorts

f : τ α f (1) × • • • × τ α f (k f ) → τ α f (0)
2. A unique constant "X":τ 0 denoting the object domain under analysis;

For each Split

c : D αc) → n∈N D αc ∈ S and each n ∈ N, a function symbol c n : τ αc → τ αc .
The set of ground terms over Σ F,S is as usual the least set T(Σ F,S ) such that:

• "X":τ 0 ∈ T(Σ);

• if t 1 :τ 1 , . . . , t k f :τ k f ∈ T(Σ) and f : τ α f (1) × • • • × τ α f (k f ) → τ α f (0) then f (t 1 , . . . , t n ): τ α f (0) ∈ T(Σ); • If t : τ ∈ T(Σ), t = c n (t ) for some n ∈ N, then for all m ∈ N, c m (t) ∈ T(Σ).
The last rule prohibits the application of a split function on a class that is the result of the application of the same split function. In most cases the specific set of functions is not relevant to the analysis, and we denote simply Σ a sorted first-order functional signature as defined above.

Positions and subterms.

A position is a finite sequence of integers, with denoting the empty sequence. Positions in and subterms of a term t are defined recursively as follows:

• t is a subterm of t at position ;

• If f(t 1 , . . . , t n ) is a subterm at position p in t, then each t i is a subterm at position p • i in t.
Given a term t we denote Sub(t) its set of subterms.

Representation and object terms. The terms t : τ such that τ = α f (0) for a representation function f are called (ground) representation terms. Otherwise they are called (ground) object terms. Given a set of terms S we denote Repr(S) the subset of representation terms in S.

Interpretation of u ∈ D 0 . The interpretation of a function symbol f is denoted [ [f] ]
and is f . The interpretation of a term t over u ∈ D 0 is denoted [ [t] ] u and defined inductively on ground terms as expected:

   [ ["X"] ] u = u [ [f(t 1 , . . . , t n )] ] u = f ([ [t 1 ] ] u , . . . , [ [t n ] ] u ) [ [c n (t)] ] u = Split c ([ [t] ] u )(n)
If t is a representation term we distinguish its interpretation on u by calling it a value and denoting it Val u (t)). The codomain of Val u (t)) is denoted coDom(t).

Data Exchange Systems (DXS)

A DXS is a set of terms over a signature Σ = Σ F,S . with a few conditions that we explicit in this section. Definition 2. (Data Exchange System) Let Σ be a signature. A Σ-Data Exchange System (Σ-DXS) is a non-empty set of ground terms S ⊆ T(Σ) such that:

• "X" ∈ S;

• Each term t ∈ S is the result of the application of a function in Σ on a finite subset of S;

• If c n (t) ∈ S, then for all m ∈ N, c m (t) ∈ S.
We denote D(Σ) the set of Σ-Data Exchange Systems.

The initial DXS ⊥ D(Σ) is {"X"}. Given two possible DXS S,S we denote S S if S ⊆ S as sets. D(Σ) with a poset with the ordering and the join operation ∆ ∆ = ∆ ∪ ∆ . Let us prove it is a domain. First we note it has a maximal element, T(Σ) and a minimal element, the initial DXS. Per definition they are a closed subset of the powerset of the set of terms, and thus lattices. It remains to prove they are algebraic.

Consider a cognition Add t that adds a term t to a DXS, or if t is one of the result of a split function c on a term t, adds simultaneously all the possible results c n (t). Let C Σ be the set of all these cognitions. The constraint on the addition of terms in the definition of DXS, namely that before a term is added all its subterms must be present, naturally orders the set C Σ with Add t ⊆ Add t whenever t (or one of the cases if t denotes the application of a split function) is a subterm of t . Reusing the discussion on the construction of object domains, it is then natural to consider the algebraic lattice L CΣ , or more simply L C if Σ is clear from the context, of ideals of C Σ . Given that the elements of L C are exactly the allowed constructions for DXS, we have the following proposition, which in turn entails that D(Σ) is also an algebraic lattice.

Proposition 4. L CΣ is isomorphic (as a lattice) to D(Σ).

As a corollary the compact DXS are the images of finite sets of cognitions in C Σ .

Since DXS are domains it is possible to define morphisms on DXS domains to extend the signature with new morphisms or split functions obtained either Technical report No. IRIT/RR-2022-08-FR https://www.irit.fr/ Yannick.Chevalier/ -Yannick.Chevalier@irit.fr through user-interaction (a case of teaching) or through the system's own cognitions.

Proposition 5. (Teaching) Let Σ, Σ be two representation signatures such that Σ ⊆ Σ . Then the identity injection: ι : D(Σ) → D(Σ ) is an algebraic morphism.

The morphism on signatures (as denumerable sets of symbols) adding a new function is clearly algebraic. It shall be noted that the construction presented so far to define learning encompasses experience through the observations, studying through the cognitions, and being taught through signature extensions. This delineation is informal: On the one hand, concepts learned from a preliminary analysis can lead to the addition of a new split function, and the detection of a functional relation between terms can lead to the addition of a new function to the signature without any interaction or "being taught". On the other hand the role of categories in Kant's analysis, especially in relation with the table of judgements, is one functions that hold together several objects to produce a new one, and some of these categories are assumed to be innate. Functions in the signatures are those categories that hold together the objects of perception regardless of whether they are innate, taught, or infered by cognitions.

Practical Knowledge and Skills

Knowledge has already been defined many times in many different settings. It seems nonetheless appropriate to add two new definitions. In this section Practical Knowledge is the valuation of representation terms. The skill steming from that knowledge is the ability to detect anomalies, a process called monitoring. In essence, algebraicity entails that the set of all possible observations can be approximated by finite observations; Continuity then imply the convergence of the valuation learned to that of the ideal representation. The system is self-correctible when given labeled observations.

Practical Knowledge

First we prove that the valuation of terms in a domain is continuous as it is the composition of continuous functions. Let Σ be a signature, S be a DXS in D(Σ), D be a domain, u be an observation, and t be a term. These notations are decorated reasonably, and D 0 is the domain on which "X" is interpreted.

Lemma 1. The mapping u ∈ D 0 → [ [t] ] u is an algebraic morphism.
Proof. By contradiction assume the set Ω of terms t such that the mapping u ∈ D 0 → [ [t] ] u is not continuous is not empty. Let t be minimal for the well-founded subterm relation in Ω. We must have t = "X". If t = f (t 1 , . . . , t n ), then by minimality of t the functions u → [ [t i ] ] u are continuous, and thus by function composition the function u → [ [t] ] u must be continuous as both morphisms and split functions are continuous, a contradiction. Algebraic functions map compact to compact, thus their finite compositions are algebraic.

In the following proposition, since the mapping to each coordinate is continuous by Lemma 1, the mapping to the product of interpretations is continuous. Proposition 6.

Val S : D 0 → t∈Repr(T(Σ)) coDom(t) u → t∈Repr(T(Σ)) d t with d t = Val u (t) if t ∈ S ⊥ coDom(t) Otherwise is a morphism. It is algebraic if S is compact.
Proof. We have already seen that the codomain t∈Repr(T(Σ)) D(t) is in aLAT ! . By Lemma 1 the projections to each coordinate are continuous. Thus by the universal property of the product topology this function is continuous. Also it clearly maps to the product of the minimal elements, which is the minimal element of the product.

It remains to prove it is algebraic when S is compact. Assume this is the case and let u ∈ D 0 be an observation. Since u is compact it contains a finite number of events. Since S is compact, it contains only a finite number of non-split terms, and a finite number of splits (each of which adding a denumerable number of terms). By Prop. 3 and since u is compact for each split only a finite number of terms have a non-bottom valuation.

Thus if S is compact, all but finitely elements of the product have the ⊥ valuation, the remaining ones having a compact value since the interpretation of each term is compact by Lemma 1.

The valuation is also continuous if the DXS changes with a fix world u.

Proposition 7.

Val u :

D(Σ) → t∈Repr(T(Σ)) coDom(t)) S → Val S u is a morphism. It is algebraic if u is compact.
Proof. "X" is not a representation term and thus Val u maps the bottom element of D(Σ) to the bottom element of the product. Its continuity again is derived from the fact that the mapping to each coordinate t is continuous as it can only change once from

⊥ D(t) to Val D(t) ([ [t] ] u ).
When u is compact, the fact that it maps compact DXS to compact elements of the product is already proved in the proof of Prop 6.

A function continuous in each argument being continuous on the product, we obtain the following theorem that characterizes our learning approach.

Theorem 1.

Val :

D 0 × D(Σ) → t∈Repr(T(Σ)) coDom(t)) (u, S) → t∈Repr(T(Σ)) Val S u (t) is algebraic and continuous.
Proof. Continuity stems from the continuity on each argument as in Propositions 6 and 7. Algebraicity also, remembering that the compact elements of a finite product are the products of compact elements and that the minimum of the product is the pair of bottom elements.

We define practical knowledge after observing u and applying the cognitions leading to S as Val S u . By Theorem 1 knowledge is exactly that which has been learnt.

Skill: Anomaly Detection

In order to present the monitoring skill, it is adequate to introduce a few notations. Let u lim ∈ D 0 be the ideal that contains all possible observations that contain no anomaly. It is assumed that learning is based on an observation u u lim . Assuming the signature is fixed, it is possible to define a limit valuation. Definition 3. the limit valuation is Val Repr(T(Σ)) u lim . Example 6. In our running example, the table of runs would contain all the possible runs, past, present, and future, and the minimum time would be the minimum amount of a time a human can run on 100m.

Since learning is continuous the valuation learnt after an observation u approximates the limit valuation and thus is a provisory estimate. Monitoring is the act of checking that an observed world u, which is not necessary a possible one, is within the limits learned. Monitoring is a classification problem with two classes. Remembering that 1 0 an observation contains a new behaviour whenever one of the possible representations is outside the bounds reached during learning. Definition 5. (Monitor) Let Σ be a signature. Then for r ∈ t∈Repr(T(Σ)) D(t), the r-monitor is the mapping:

M r : D 0 → B u → t∈Repr(T(Σ)) Val u (t) r t
In the following lemma algebraicity is trivial as the two elements of B are compact, and continuity follows from the continuity of the valuation function (Lemma 1).

∈ D 0 → M r (u) ∈ B is algebraic.
Note that in Proposition 8 the r-monitor is fixed. We leave to the reader that reusing the notations of Prop. 8 the function: ψ u : r → M r (u) is not continuous. This fact is exploited in the next section.

Example 7. Assuming that after an observation u a minimum time for sprinting on 100m by human is computed to be 9s58, and that an event of a run in 9s is observed. The monitor function maps that event to 0, and it is thus considered as anormal, to be treated depending on the context.

As this paper generalises the setting in [START_REF] Chevalier | Data Exchange for Anomaly Detection: The Case of the CAN Bus[END_REF] we refer to that paper for assessing the effectiveness in practice of this approach for anomaly detection.

Improving skills

Recall any non-anomalous observation u should be smaller than u lim . Accordingly a world u u lim is an anomaly. An anomaly

u is Σ-detectable if M Val Repr(T(Σ)) u lim (u) = 0. It is a r-false negative if M r (u) = 1.
Finally we say that u u lim is a r-false positive if M r (u) = 0, i.e., it lies in the gap between the learnt valuation and the limit valuation.

Angluin-like [START_REF] Angluin | Learning Regular Sets from Queries and Counterexamples[END_REF] is synonymous with the possibility to converge to the right solution whenever false positive and false negatives examples to a proposed solution are given. The following theorem indicates that an Oracle can guide the system in the convergence to the limit valuation. In the first case it is only stated that a term exists. However we note that in settings in which [START_REF] Chevalier | Compiling and Securing Cryptographic Protocols[END_REF] can be employed this computation automatable. Proof. By the algebraicity and continuity of the monitor fonction. We prove the first case, the second one can either be proved similarly or by taking

u = u + v. Since v is Σ-detectable, M Val Repr(T(Σ)) u lim (v) = 0. Since it is a r-false negative, M Val Repr(S) u (v) = 1.
Since the function Val is algebraic continuous by Theorem 1, by considering an increasing chain of compacts (u , S ) above (u, S) and whose supremum is (u lim , T(Σ)), there exists a compact DXS (u , S ) such that u u , S ⊆ S , and M Val Repr(S )

u (v) = 0. Since
(v) = 0.

Conclusion on learning and monitoring.

The continuity of the learning process established in Theorem 1 implies the eventual convergence of the result of our learning algorithm towards an ideal description of the system. Theorem 2 precises how to eliminate false positives-by learning more traces-,and false negativesby adding new terms to the DXS.

Conceptual Knowledge in the Finite

Practical knowledge is useful for anomaly detection but does not address the discursive part of logic as presented in [START_REF] Longuenesse | Kant and the Capacity to Judge: Sensibility and Discursivity in the Transcendental Analytic of the Critique of Pure Reason[END_REF], namely that the mental state built through cognitions is the basis of discurse. While objects of perceptions and language are shared reality, the practical knowledge is subjective. The unity of self is the constraint that in particular names and relations in the shared language should be given a semantics consistent with the shared reality of the objects of perception. The concepts underlying this semanticisation are defined in this section as predicates of experience and domain of experience. The conceptual knowledge is the first-order model defined by these predicates and this domain.

Additional notations. Let X be a set of sorted variables denoted x, y, . . ., and decorations thereof. A term t is a term in the signature T(Σ ∪ X ). The set of variables occuring in t is Sub(t) ∩ X . A term t is a pure representation term if all functions in the definition of t are representation functions.

Outline. A state is a couple (u, S) where u is an element of D 0 and S is a DXS. Concepts are introduced through new cognitions that enrich a cognition state. These cognition states are states extended with a subset O ⊆ S of ground object terms an observer is aware of when reasoning and a set R of pure representation terms through which these objects are classified. A first-order model is built by concept analysis on the object terms as objects and pure representation terms as attribute. The truth of a pure literal l in relation with an observation u is defined through one or several substitutions θ such that lθ is ground and satisfied by u. Given a family of cognitive states (K f ) f ∈F the supremum of the family is denoted f ∈F K f and is the cognitive state K = (u, S, O, R) where:

Cognitive states

       u = ∪ f ∈F u f S = ∪ f ∈F S f R = ∪ f ∈F R f O = ∪ f ∈F O f
By altering the construction in Sec. Section 3.2 it is clear that the set of cognitive states is a domain, i.e., an algebraic lattice. The set of cognition functions is extended with cognitions Add O t adding the term t to O (with Add t Add O t to ensure that only terms in S can be added, and Add R t to add pure representation terms to R. As a consequence cognitive state K = (u, S, O, R) is compact whenever u and S are compact, and O and R are finite.

Relational signature of a cognitive state

Given a cognitive state K = (u, S, O, R) and t ∈ R let Gr K (t) ⊆ Gr O (t) be the set of substitutions θ such that tθ ∈ S. The set of substitutions defined in a cognitive Technical report No. IRIT/RR-2022-08-FR https://www.irit.fr/ Yannick.Chevalier/ -Yannick.Chevalier@irit.fr state K is denoted Subst(K) and is the set ∪ t∈R Gr K (t). Given a substitution θ ∈ Subst(K), we let Obs K (θ) be the set of observations that can be made on the objects in the image of θ:

Obs K (θ) = {t ∈ R | θ ∈ Gr K (t)}
We extend this notation to sets of substitutions with:

Obs K (Θ) = ∩ θ∈Θ Obs K (θ)
Example 8. Let K = (u, S, O, R) be a cognitive state, f : T → T D be a representation function, and eq : T D × T D → {0, 1} be an equality function, i.e., such that eq(u, v) = 1 if and only if u = v. The representation term eq(f (x), f (y)) is a binary predicate. Let Θ be the set of substitutions θ = {x → t 1 , y → t 2 } with t 1 , t 2 ∈ O such that eq(f (t 1 ), f (t 2 )) = 1. By definition we have eq(f (x), f (y)) ∈ Obs K (Θ). Knowing that the predicate must be reflexive, symmetric, and transitive can help in the computation of Θ, and symmetrically the knowledge of a maximal set of substitutions Θ leads to the learning from experience that the predicate is reflexive, symmetric, and transitive. These cognitive aspects are out of the scope of this paper, but the construction of rules from table contents given in [START_REF] Phokion | Knowledge Refinement via Rule Selection[END_REF] can be employed.

Since the set Obs K (Θ) represents the common qualities of the objects related by the substitutions in Θ predicates of experience as a subset A of particular aspects of these common qualities. Definition 10. (Predicate of Experience) Let K be a cognitive state, and Θ ⊆ Subst(K). The predicate of experience defined by Θ and A ⊆ Obs K (Θ) in K is denoted Obj A K (Θ) and is the formula:

Obj A K (Θ) =    1 If A = ∅ t∈A t θ∈Θ Val u (tθ) Otherwise
Its arity is the cardinal of ∪ t∈A Var(t). The set of predicates of experience of a set of substitutions Θ is denoted Obj K (Θ).

We denote Obj E (K) the set of predicates of experience Obj A K (Θ) for Θ ⊆ Subst(K) and A ⊆ Obs K (Θ). Gr K is extended to literals, and to predicates with Gr K ( t∈T t d t ) = ∩ t∈T Gr K (t). We give the usual semantics to the conjunction by defining the

support of ϕ = t∈T t d t in K as ∩ t∈T Supp O u (t d t ), and denote it Supp O u (ϕ). By construction Θ ⊆ Supp O u (ϕ) for ϕ ∈ Obj K (Θ): a predicate defined by the examples in Θ is satisfied by these examples. It is trivial that if θ ∈ Supp O u (Obj Obs K (Θ) K (Θ)) then θ ∈ Supp O u (ϕ) for all ϕ ∈ Obj K (Θ). That case is denoted θ ∈ Supp O u (Obj K (Θ))
, and extended to sets fo substitutions Θ .

That a set of substitutions may entail the object formulas of another set of substitutions yields a pre-order on these sets. In turns the pre-order yields an equivalence relation between sets of substitutions. Definition 11. (Specialisation) Let K be a cognitive state, and Θ, Θ ⊆ Subst(K). We say that Θ specialises Θ, and denote

Θ K Θ , if Θ ⊆ Supp O u (Obj K (Θ)
). The sets Θ, Θ ⊆ Subst(K) are K-equivalent, and we denote

Θ ≡ K Θ , if Θ K Θ and Θ K Θ.
The equivalence classes for ≡ K are (pre-order) isomorphic with the predicates of experience on K. Lemma 3. Let K = (u, S, O, R) be a cognitive state, and Θ, Θ ⊆ Subst(K) be such that Θ ≡ K Θ . Then Obj K (Θ) = Obj K (Θ ).

Proof. Let Θ, Θ ⊆ Subst(K) be such that Θ K Θ . It suffices to proves Obj

Obs K (Θ) K (Θ) = Obj Obs K (Θ ) K (Θ ).
By definition Θ K Θ implies Obs K (Θ ) ⊆ Obs K (Θ), and thus by double inclusion Θ K Θ implies Obs K (Θ) = Obs K (Θ ).

By definition of

K for each θ ∈ Θ we have u |= Obj K (Θ)θ . For each r ∈ Obs K (Θ), u |= Obj K (Θ)θ implies Val u (rθ )
θ∈Θ Val u (rθ). Inversing the roles of θ, θ we also get that for all r ∈ Obs K (Θ ), and all θ ∈ Θ we have Val u (rθ) θ ∈Θ Val u (rθ ). Taken together these inequations yield for all r ∈ Obs K (Θ):

θ∈Θ Val u (rθ) = θ ∈Θ Val u (rθ )
Given the two preceding paragraphs and the definition of Obj K we have:

Obj K (Θ) = Obj K (Θ ).
Conversely, Obj K (Θ) = Obj K (Θ ) implies, together with the fact that by construction u |= Obj K (Θ)θ for all θ ∈ Θ , and symmetrically when reversing the roles of Θ and Θ , that Θ ≡ K Θ . This tight coupling is employed to transfer the predicates of experience between cognitive states through the sets of substitutions and representations that generate them.

Domain of a cognitive state

The construction of a domain from a cognitive state K = (u, S, O, R) proceeds by considering the elements of O modulo an equivalence generated by Obj E (K). This approach has two obstacles:

• A first modeling problem is whether it suffices to consider all comparisons between terms in O in the image of the possible substitutions, or if all the replacement of one term by another in O have to be considered. Both choices lead to an equivalence relation on O, the latter making it a congruence on terms. Lemma 5 provides the proof of termination of the replacements though to ease notations only the changes in the codomain of the substitutions are considered outside of the corresponding paragraph, with hints for the non-obvious adaptations;

• A second problem is that pairwise comparison of terms does not yield a transitive relation as some terms may be missing in S. Instead of considering all intermediate cognition states as described by Kant, we introduce the notion of stable state to indicate that all the needed replacements have been performed.

Example 9. Importance of transitivity for proper reasoning. It can be determined that a witch weights the same as a duck by considering successively that people burn witches and wood, that wood and ducks float on water, and that the weight of an object determines whether it floats. The cognitive state on which this reasoning is sensible lacks transitivity as it is not determined whether people burn ducks nor whether witches float. It is thus not stable, and additional experiences (construction of new terms) are needed to make it stable. Out of the scope of this paper, it would be also sensible to determine whether floating on water is a good characterisation of witches as a special subset of humans.

Considering closure under replacements. The following lemma allows for the transfer of a replacement on an instantiated term to a replacement on the substitution, and is used without references when considering ground instances of pure representation terms.

Lemma 4. Let t be an object term, r be a pure representation, and θ be a substitution such that rθ is ground. Then if (rθ) |p = t and p ∈ Pos(r) then r |p is a variable.

Proof. Since t is an object term the symbol at position in t denotes an object morphism. Since r is a pure representation term, this symbol cannot occur in r.

Thus t can occur in rθ only at a position of a variable or below.

Definition 12.

A set of ground terms O is replacement saturated if for all t, t 1 , t 2 ∈ O and position p ∈ Pos(t), we have either

t |p = t 1 implies t[p ← t 2 ] ∈ O or t |p = t 2 implies t[p ← t 1 ] ∈ O.
The replacement saturation of a set of terms can be computed effectively and is finite. Proof. Let < be a simplification ordering [START_REF] Dershowitz | Rewrite Systems[END_REF] on terms. We consider the ground term rewriting system T = {t → t | t, t ∈ O and t < t}. The Knuth-Bendix completion of T always succeed (Corollary 6.2 in [START_REF] Kapur | The Knuth-Bendix Completion Procedure and Thue Systems[END_REF]) and yields a finite equivalent term rewriting sytem T . Let O be the set of terms that contains O and such that t ∈ O and t → T t implies t ∈ O . Since T is always terminating this set if finite, and it is replacement saturated by definition.

Proper construction of the domain. From now on we only consider the replacement in the codomain of substitutions of one term with another term. This replacement may be partial. Given a substitution θ of support X, for Y ⊆ X and t, t terms we denote θ[t ← t ] Y the substitution:

θ[t ← t ] Y (x) = θ(x) if x / ∈ Y t if x ∈ Y and θ(x) = t
The following definition can be adapted by furthermore assuming O is replacement saturated and considering the orbits for the symmetric closure of the t → t rewriting rule: the terms t and t are equivalent if and only if the valuation is constant over the orbit of each representation term.

Conversely assume that for all Θ ∈ Subst(K) and all X ⊆ ∩ θ∈Θ Dom(θ) we have

Obj K (Θ) = Obj K ({θ[t ← t ] X | θ ∈ Θ}) By Lemma 3 Obj K (Θ) = Obj K ({θδ t,t | θ ∈ Θ} ∩ Subst(K)) is equivalent to Θ ≡ K {θ[t ← t ] X | θ ∈ Θ}.
In particular for all θ ∈ Θ and for all r ∈ R such that θ ∈ Gr K (r) that Val S rθ[t←t ] X ( ) Val S u (rθ), and thus again by Definition 13 that t ≡ o K t .

Next lemma is a direct consequence of Definition 13 that is highlighted for further reference.

Lemma 7. Let K = (u, S, O, R) be a compact stable state and t 1 , t 2 ∈ O such that t 1 ≡ o K t 2 .
Then for all θ ∈ Subst(K), for all X ⊆ Dom(θ), and for all r ∈ Obs K (θ

) we have rθ = rθ[t 1 ← t 2 ] X .
Thus the truth value of predicates of experience can be defined on the equivalence classes of ≡ o K . This approach fails to take into account that there exists objects not in O. Accordingly given the domains D 0 , . . . , D n let Others = {other D } D∈{D0,...,Dn} be a set of constants each interpreted in its labeling domain as the bottom of that domain. Even if different terms in an equivalence class may have different interpretation, Lemma 7 implies when considering predicates of experience, the choice of the representative in indifferent. Thus these two sets of constants together define a domain on which predicates of experience can be evaluated. Valuation on Dom(K). We denote the valuation on Dom(K) with Val K and define:

Val K (a) = ⊥ Di If a ∈ Others of sort τ i Val u (t) for any t ∈ a otherwise

Conclusion

By Lemma 7 the valuation of an instantiation of a term r ∈ R never depends on the term chosen in the equivalence class. This allows the extension of substitutions to the domain of a cognitive state.

(Dom(K), Obj E (K), |= K ). Given P ∈ Obj E (K) of arity n we denote |= K P (a 1 , . . . , a n ) iff θ = {x i → a i } 1≤i≤n ∈ Supp O u (R).
A preliminary of conceptual knowledge for a stable compact cognitive state K is Mod(K). be an inverse system of models. Let ∆ ⊆ f ∈F D f be the set of all ξ such that f ≥ f implies g f ,f (ξ(f )) = ξ(f ). Then ∆ is the set of threads of M. Definition 21. (Predicates of an inverse system of models) Let F be a directed poset and

M = ((M f = (D f , R f , |= f )) f ∈F , (g f ,f ) f f , (ϕ f ,f ) f f )
be an inverse system of models. Let P ⊆ f ∈F R f be the set of all ρ such that f ≥ f implies ϕ f ,f (ρ(f )) = ρ(f ). Then P is the set of predicates of M.

Definition 22.

(Inverse Limit of an Inverse System) Let F be a directed set and

M = ((M f = (D f , R f , |= f )) f ∈F , (g f ,f ) f f , (ϕ f ,f ) f f )
be an inverse system of models. Let ∆ be the set of threads of M and P be its set of predicates. Let M = (∆, P, |= M ) be a model where

|= M ρ(ξ 1 , . . . , ξ n ) if for all f ∈ F we have |= f ρ(f )(ξ 1 (f ), . . . , ξ m f (f )) with m f ≤ n being the arity of ρ(f ).
Then M is the inverse limit of the inverse system M.

In [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF] the proof of the equivalent theorem relies on Tychonoff's Theorem and contingent considerations on threads. It is better viewed as a generic domain result. Indeed each mapping in

((D f ) f ∈F , (g f ,f ) f f ) and ((R f ) f ∈F , (ϕ f ,f ) f f
) is a projection, and taking the lower adjoints of these defines two expanding systems with the indicated limit by Theorem 3.3.7 in [START_REF] Abramsky | Domain Theory[END_REF].

f = (D f , R f , |= f )) f ∈F , (g f ,f ) f f , (ϕ f ,f ) f f
) be an inverse system of models of inverse limit M = (∆, P, |= M ). Then M is not empty.

The inverse limit as defined in Definition 22 is consistent with our definition of models for stable compact cognitive states. Lemma 11. Let K = (u, S, O, R) be a stable compact cognitive state. Then M odel(K) is isomorphic with the inverse limit of:

(Mod(K )) K ∈K↓ , (h K ,K ) K K ∈K↓ , (ψ K ,K ) K K ∈K↓ )
Proof. Since K is compact the projections define predicates and threads unambiguously: e.g., for every thread xi in the domain of the inverse limit one has ξ(K ) = h K ,K (ξ(K)). The model homomorphism property of inverse system entails that the interpretation of the limit in the inverse system is the same as that in Mod(K).

Lemma 11 allows the proper definition of conceptual knowledge for all stable cognitive states.

Definition 23. (Conceptual Knowledge)

The conceptual knowledge in a stable cognitive state K is denoted Mod(K) and is the inverse limit of the inverse system of models:

(Mod(K )) K ∈K↓ , (h K ,K ) K K ∈K↓ , (ψ K ,K ) K K ∈K↓ )

Transcendental model

Remembering that u lim ∈ D 0 contains all the possible observations of a system, it is possible to define the model for transcendental logic given the possible observations and cognitions. Definition 24. (Transcendental Model) Let D 0 be an object domain, u lim ∈ D 0 be the ideal containing on all possible observations, Σ be a signature of morphisms available for reasoning, and X be a denumerable set of variables. Then the model for transcendental logic on (u lim , Σ) is the inverse limit of the K-inverse system of models with K = (u lim , T(Σ), T(Σ) \ Repr(T(Σ)), R), with R the set pure representation terms in T(Σ ∪ X ).

Building on [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF] this model is of practical interest, as the observed system can be partially specified with universally quantified implications between positive formulas, called geometric rules. In particular it was observed in [START_REF] Guttman | Establishing and preserving protocol security goals[END_REF] that deduction systems commonly employed for the symbolic analysis of cryptographic protocols, and in particular in static equivalence analysis, are examples of such theories.

Conclusion

The aim of this paper was to solve two challenges. A first one is to fill the gap in the formalisation of transcendental logic in [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF] to precise how cognitions are achieved from experiences and cognitions, which is achieved in Definition 24. Having a first complete formalisation at hand to understand Kant's work opens the possibilities (i) of more concrete discussions on how to alter (or reject) that model to describe more precisely Kant's analysis of humans' thought process; (ii) of given a proper semantics to a natural language with names presented through examples; and (iii) interpreting the table of judgements of [START_REF] Kant | Critique of the Pure Reason ; Translated from the German by Paul Guyer and Allen W. Wood[END_REF] as morphisms operating on different aspects a cognitive state. In particular the analysis of the relations between observations is not explored in this paper.

A second one was to provide a formal framework for anomaly detection in the context of intrusion detection systems. Until further work proves otherwise, modeling learning with morphisms on domains prevents the usage of most common Machine Learning algorithm. Despite this limitation, this setting is still applicable to at least some anomaly detection problems as it formalises [START_REF] Chevalier | Data Exchange for Anomaly Detection: The Case of the CAN Bus[END_REF]. In these cases we believe that it fills partially the gap described in [START_REF] Sommer | Outside the Closed World: On Using Machine Learning for Network Intrusion Detection[END_REF] between what ML algorithms provide and what is actually needed for anomaly detection, and in particular the main recommendation of understanding what the system does.

We provide more details with references to the corresponding section of [START_REF] Sommer | Outside the Closed World: On Using Machine Learning for Network Intrusion Detection[END_REF].

Based on the practical knowledge synthesis, (III-A) outlier detection can be achieved at least in some cases [START_REF] Chevalier | Data Exchange for Anomaly Detection: The Case of the CAN Bus[END_REF], and the (B) high cost of error can be addressed over time by Theorem 2. Conceptual knowledge is only the first step towards reducing the (III-C) semantic gap. Further work is needed to align the profusely created predicates of experiences with human-understandable concepts. In particular we believe that addition of object and representation terms in the cognitive state is driven by this process.

As it is a first-order model it is trivial to add rules (implications between geometric given the results of [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF]) describing either normal behaviours or possible attack scenarios. A missing part is the relation between these rules and the application of morphisms to check their validity. It is notable that dynamic proofs in [START_REF] Coquand | A Completeness Proof for Geometric Logic[END_REF] add facts to construct a model. When building a theory of a system, these facts have to be checked, i.e., the terms and predicates of experience have to be constructed.

It fits the demands in IV-D-2) on result understanding as follows: Being complete lattice morphisms our learning algorithms all have an upper adjoint that provides a minimal explanation (as the meet of all viewed observations that lead to the current state) for each computed value. Ultimately the composition of these explanations provides an observation that explains the decision. Lemma 12. Assume the purely parallel process P = while true do (A 1 ; . . . ; A n ) is executed on the network, that the trace u is observed, and that P is unambiguous for u. Then for all 1 ≤ i < j ≤ n and for all t ∈ A i , t ∈ A j we have:

|[ [t ] ] u | = |[ [t] ] u | or |[ [t ] ] u | = |[ [t] ] u | + 1
Proof. We first prove the following statement that is satisfied by the less constrained process: P = while true do (∪ n i=1 A i )

Claim. For every trace u there exists L u , H u , and E u such that:

• L u , H u is a partition of ∪ n i=1 A i and L u =; • E u ⊆ ∪ n i=1
A i is the subset of the terms of the process that have not been observed in the current iteration of the process;

• The following equalities are satisfied:

       ∀t, t ∈ L u , |[ [t] ] u | = |[ [t ] ] u | (A) ∀t, t ∈ H u , |[ [t] ] u | = |[ [t ] ] u | (B) ∀t ∈ L u , ∀t ∈ H u , |[ [t] ] u | + 1 = |[ [t ] ] u | (C) E u = L u (D)
Proof of the claim. By induction on the length of the trace u. -If e / ∈ ∪ n i=1 ∪ t∈Ai [ [t] ] u•e , i.e., the observed event e is not associated with a term in the process, then setting L u•e = L u , H u•e = H u , and E u•e = E u satifies the constraints of the claim; -Otherwise there exists t ∈ ∪ n i=1 A i such that e ∈ [ [t] ] u•e . Since the process is unambiguous the term t has not been observed in the current iteration of the loop, and thus t ∈ E u . By induction this implies t ∈ L u . One then easily checks that the equalities are all satisfied by setting: *

• If u = ε let H ε = ∅ and L ε = E ε = ∪ n i=1 A i . Since H u = ∅
If L u = {t}: L u•e = E u•e = ∪ n i=1 A i and H u•e = ∅; * Otherwise L u•e = L u \ {t}, E u•e = L u•e ,
≤ i t ≤ n such that H u ⊆ ∪ it i=1 A i , L u ⊆ ∪ n i=it A i , and if E u = E u•e there exists t ∈ L u ∩ A it such that e ∈ [ [t] ] u .
The proof is a copy of the one of the first claim, but it has been separated for clarity. One has to observe that to respect the sequentiality of the process, when t ∈ E u ∩ A j is chosen we must have E u ∩ ∪ j-1 i=1 A i = ∅. The Lemma follows from the two claims by case analysis on the repartition of t, t in H u and L u using the second claim to transform it into a case analysis on the indice. Proposition 10. Let S be a DXS with a classification set S c , and u be a trace. Assume the purely parallel process P = while true do (A 1 ; . . . ; A n ) is executed on the network, and that P is unambiguous for u. Then for every t ∈ A i , t ∈ A j with i > j we have P u Sc (t, t ) = 1.

The other direction cannot be proven as a purely parallel process can be found by coincidence when there are few iterations of the loop.

We present in Fig. 1 examples of the analysis result on a Model 3 CAN Bus log [START_REF] Wardell | Log of a Tesla Model 3 Car[END_REF] representing 418s of execution and 879682 frames. Figure 1: Examples of purely parallel processes found on a Tesla Model 3 log. In total 29 CAN frames id were isolated, 32 were discovered in a request-response process, and 126 involved were in a star process either proper as in Fig. 1a or degenerate as in Fig. 1b.

A.2 Discovering Protocol Instances

Setting.. A protocol is a program running among multiple participants in a network and observed through the messages exchanged by these participants. It is specified with a set of roles that are programs and the execution of a role is a process called an actor. In addition to the control rules defined in the role an actor is playing, the actor has a local memory that is updated while running the protocol. We note that as in [START_REF] Chevalier | Implementing Security Protocol Monitors[END_REF] under this definition a multi-step attack in which an adversary communicates with different actors on the network is also a protocol.

As in [START_REF] Laraba | Mitigating TCP Protocol Misuse With Programmable Data Planes[END_REF] each role is modeled with an Extended Finite State Machine (EFSM), a finite state automaton enriched with rules updating the state of an actor playing that role. This automaton is deterministic in the sense that an actor playing a role and receiving a message can either reject that message as non-conforming with the protocol specification and leaves its state unchanged, or change its state according to the rules set in the rule in exactly one possible way. Thus to each state of the automaton we associate a couple of functions (g, p) where g returns whether a message received in the current participant's state is acceptable, and p that performs the update of the memory and of the automaton state. A group of actors playing the roles defined in the protocol and communicating one with another is called a session.

More formally let X be a finite set of sorted variables, R be a finite set of Technical report No. IRIT/RR-2022-08-FR https://www.irit.fr/ Yannick.Chevalier/ -Yannick.Chevalier@irit.fr constants (the roles), Q be a finite state of automaton states, and E be the set of the possibly observed events (the messages). A memory state is a ground substitution of domain X. We denote M the set of possible memory states. A state is a couple (q, σ) ∈ Q × M. A guard is a function Q × M × E → B. A posttransition is a function Q × M × E → Q × M × E. If p is a transition function and f (q, m, e)) = (q , m , e ) then upon receiving the message e, the actor with a state (q, m) updates it to (q , m ) and sends the message e .

An EFSM E is a set of tuples {(q, g q , f q )} q∈Qr⊆Q where g q is a guard and f q is a post-transition function. A protocol P is a finite set of tuples {(r, ι r , E r )} r∈R where each E r is an EFSM, ι r ∈ Q is the initial state of the role r, and if r = r then Q r ∩ Q r = ∅. The bin role contains one state Q b = {ι b }, and one rule (ι b , g b , f b ) where the guard g b is always true and f b does nothing.

Algorithm.. Again we build a representation of the system inductively on a trace u. Let P = {(r, ι r , E r )} r∈R be a protocol. Participants are identified uniquely and are assumed to always or never play a role of the protocol. Depending on the network type they can be identified by a socket address or in the case of the CAN bus by the id of the frame. Actors are participants playing a role in the protocol. We first build a derived object simulating the network after observing a trace u Our representation of the network is based on an internal state A u of potential actors with their state. Accordingly we let: A(ε) = {(ι p,r , m p,r , E p,r )} (p,r)∈P×R assuming initially every participant may play a role in the protocol.

Inductively the internal state of the function is defined as follows:

• If there exists (q p,r , m p,r , E p,r ) ∈ A(u), a transition (q p,r , g qp,r , f qp,r ) ∈ E p,r , and an event e ∈ u such that:

g qp,r (e , m p,r ) = 1 f qp,r (e , q p,r , m p,r ) = (e, q p,r , m p,r )

Then:

A(u • e) = (A(u) \ {(q p,r , m p,r , E p,r )}) ∪ (q p,r , m p,r , E p,r )

• Otherwise the participant has sent a message that is not conformant with the protocol specification, and thus per our assumption never is an actor, in any role, of that protocol:

A(u • e) = A(u) \ {(q p,r , m p,r , E p,r ) ∈ A(u) | r ∈ R}

The representation of the network after observing the trace u is the subset of participants p such that there exists an EFSM indexed by p in A(u). We order these sets with A B if and only if B ⊆ A. The top element is the emptyset and the bottom element is the set of all participants, and the join A B of two sets is their intersection. This domain clearly is a representation domain. The computation of A(u) is extended to worlds with A(Σ u∈U u) = u∈U A(u), and is clearly continuous. Though it possible for a participant to play different roles concurrently and be correctly detected, playing concurrently the same role may (as in the case of a server in [START_REF] Laraba | Mitigating TCP Protocol Misuse With Programmable Data Planes[END_REF]) make the participant appear as not playing along the rules of the protocols. The benefit of this simplification is the low computational and memory cost in practice.

Our implementation of the Multi-Frame Message protocol [START_REF] Iso | Road vehicles -Diagnostic communication over Controller Area Network (DoCAN) -Part 2: Transport protocol and network layer services[END_REF] has correctly detected on the Tesla Model 3 log the similar CAN-TP [START_REF] Autosar | Specification of CAN Transport Layer[END_REF] protocol according to owners' common findings [START_REF]OBD-II Semantics of CAN Frames[END_REF].

Definition 4 .

 4 A ground literal is an expression t d where t ∈ T(Σ) is a representation term, and d ∈ coDom(t).

Theorem 2 .

 2 (Angluin-like Machine Learning) Let Σ be a signature, and (u, S) ∈ D(Σ) be a DXS. Let r = Val Repr(S) u be the result of the learning phase, and v ∈ D 0 be a world. 1. if v is a detectable anomaly and a r-false negative, there exists S such that S ⊆ S and M Val Repr(S ) u (v) = 0; 2. if v is a normal behavior and a r-false positive, there exists u such that u u and M Val Repr(S) u (v) = 1.

Definition 7 .

 7 (Grounding) Let O be a set of object terms and t be a pure representation term. A substitution θ O-grounds t if:coDom(θ) ⊆ O tθ is groundWe denote Gr O (t) the set of substitutions that O-grounds the term t. Given a set of object terms O we denote Subst(O) the set of substitutions whose codomain is included in O. As a matter of convenience this notion is extended to literals and we denote Gr O (t d) the set Gr O (t) when t is a pure representation term. Definition 8. (Support of a literal) Let O be a set of object terms and u ∈ D 0 . A substitution θ (u, O)-supports a pure literal r d if θ ∈ Gr O (r d) and Val u (rθ) d. We denote this fact with θ |= (u,O) l, and denote Supp O u (l) the subset of Gr O (l) of substitutions that (u, O)-supports the literal l. Definition 9. (Cognitive State) A cognitive state is a tuple K = (u, S, O, R) such that: • u ∈ D 0 and S is a DXS; • O ⊆ S contains only object terms and for all o ∈ O we have [ [o] ] S u = ε; • R is a set of pure representation terms; Given two cognitive states K = (u, S, O, R) and K = (u , S , O , R ) we say that K is an extension K, and denote it K K , if u u , S ⊆ S , O ⊆ O , and R ⊆ R .

Lemma 5 .

 5 Let K = (u, S, O, R) be a compact cognitive state. Then there exists a finite and unique minimal set of ground term O such that O ⊆ O and O is replacement saturated.

Definition 15 .

 15 (Domain of a cognitive state) Let K = (u, S, O, R) be a stable cognitive state. The domain of K is the set O/ ≡ o K ∪Others and is denoted Dom(K).

Definition 16 .

 16 (Model a Compact Cognitive State) Let K = (u, S, O, R) be a stable compact cognitive state. The model of K is denoted Mod(K) and is the tuple

Theorem 4 .

 4 Let F be a directed set and M = ((M

  the equations (C) and (D) are trivially satisfied. The interpretation is strict so the equation (A) is satisfied (and the length is equal to 0). The equation (D) is satisfied by definition.• Assume the claim stands for a trace u and consider the trace u • e.

  and H u•e = H u ∪ {t}; Claim. For any trace u, there exists 1

  (a) The star PPP is the most common one on the Tesla Model 3: Two sets of ids separated by a single node. This PPP is iterated 4181 times in the log.(b) A degeneracy of the star PPP is to have one of the set of nodes which is empty. This PPP is also iterated 4181 times in the log.

  Institut de Recherche en Informatique de Toulouse CNRS -INP -UT3 -UT1 -UT2J ASR -Architecture, Systems and Networks RMESS -Networks, Mobile, Embedded, Wireless, Sattelites SEPIA -Operating systems, distributed systems, from Middleware to Architecture SIERA -Service IntEgration and netwoRk Administration T2RS -Real-Time in networks and systems TRACES -Trace stands for research groups in architecture and compilation for embedded systems CISO -HPC, Simulation, Optimization APO -Parallel Algorithms and Optimisation REVA -Real Expression Artificial Life FSL -Reliability Systems and Software ACADIE -Assistance for certification of distributed and embedded applications ARGOS -Advancing Rigorous Software and System Engineering ICS -Interactive Critical Systems SM@RT -Smart Modeling for softw@re Research and Technology GD -Data Management IRIS -Information Retrieval and Information Synthesis PYRAMIDE -Dynamic Query Optimization in large-scale distributed environments SIG -Generalized information systems IA -Artificial Intelligence ADRIA -Argumentation, Decision, Reasoning, Uncertainty and Learning methods LILaC -Logic, Interaction, Language and Computation MELODI -Methods and Engineering of Language, Ontology and Discourse ICI -Interaction, Collective Intelligence ELIPSE -Human computer interaction SMAC -Cooperative multi-agents systems TALENT -Teaching And Learning Enhanced by Technologies SI -Signals and Images MINDS -coMputational Imaging anD viSion SAMoVA -Structuration, Analysis, Modeling of Video and Audio documents SC -Signal and Communications STORM -Structural Models and Tools in Computer Graphics TCI -Images processing and understanding

  Technical report No. IRIT/RR-2022-08-FR https://www.irit.fr/ Yannick.Chevalier/ -Yannick.Chevalier@irit.fr aLAT ! if D n ∈ aLAT ! for all n ∈ N..

Lemma 2 .

 2 Let Σ be a signature, and d be in coDom(t) for a representation term t. Then the function M t,d : u → Val u (t) d is algebraic. If furthermore d is compact then the function: M t,d By monotony of the valuation and 1 0 this is true if Val u (t) d = 1. Let us now assume this is not the case, and thus that Val u (t) d = 0 or equivalently that d Val u (t). function w → Val w (t) is continuous by Lemma 1 and thus Val u (t) = v∈↓u Val v (t). Since this function is algebraic all the Val v (t) values are compact. By definition of compactness, and since algebraic lattices are bounded-complete, if d Val u (t) = v∈V Val v (t) there exists v ∈ V such that d Val v (t) and thus such that Val v (t) d = 0. Let r ∈ t∈Repr(T(Σ)) coDom(t), and M r be the r-monitor. Then the mapping u

	The Proposition 8.

s : u → Val u (t) d is continuous.

Proof. Only the last statement is not trivial. Assume u = v∈V v where V contains only compact elements. We have to prove that Val u (t) d = v∈V Val v (t) d.

  we take the supremum of the values on each term, there exists a term t ∈ S such that Val v (t) Val u (t). Let us consider the possibilities for t. Since the valuation is increasing on each term, for all t ∈ S we have Val u (t) Val u (t), and thus Val v (t) Val u (t) implies Val v (t) Val u (t). Since v is a false negative, we have for all t ∈ S that Val v (t) Val u (t). Thus there exists t ∈ S \ S such that Val v (t) Val u (t), and thus Val v (t) Val u (t). Thus we have M Val Repr(S )

	u

Technical report No. IRIT/RR-2022-08-FR https://www.irit.fr/ Yannick.Chevalier/ -Yannick.Chevalier@irit.fr

https://www.irit.fr/ Yannick.Chevalier/ -Yannick.Chevalier@irit.fr

Definition 13. (Pre-order and equivalence on O) Let K = (u, S, O, R) be a compact cognitive state. Given t, t ∈ O we write t o K t if for all θ ∈ Subst(K), for all X ⊆ Dom(θ), and for all r ∈ R we have Val S u (rθ[t ← t ] X ) Val S u (rθ). We denote t ≡ o K t the fact that t o K t and t o K t.

This closure by partial replacement may seem too stringent but is technically necessary to prove transitivity in the following lemma. Lemma 6. t o K t is pre-order on O.

Proof. It is trivially reflexive. Assume t, t , t ∈ O be such that t o K t and t o K t . Let θ ∈ Subst(K), X ⊆ coDom(θ), and r ∈ R. We remark that θ[t ← t ] X = θ[t ← t ] X∩θ -1 (t) . It thus suffices to prove Val S u (rθ[t ← t ] X∩θ -1 (t) ) Val S u (rθ). By composition we have rθ[t ← t ] X∩θ -1 (t) = rθ[t ← t ] X∩θ -1 (t) [t ← t ] X∩θ -1 (t) and conclude with the hypothesis and the transitivity of .

Thus by Lemma 6 ≡ o

K is an equivalence relation on O. The behaviour of this equivalence is problematic when considering the addition of representation terms in S.

Starting from an empty set O and adding successively t 1 and t 2 makes the equivalence classes not monotonic. Accordingly stable cognitive states are those states such that S contains enough terms to properly evaluate all replacements of one term in O with another when instantiating a term in R.

Definition 14. (Stable cognitive state

The essence of the following proposition is that the equivalence class ≡ o K on O defines a finer equivalence than ≡ K on P(Subst(K)) (the first part), but that it is the coarsest equivalence on O that induces an equivalence finer than ≡ K on P(Subst(K)) (the second part). Proposition 9. Let K be a stable cognitive state, and t, t ∈ O. If t ≡ o K t then for all Θ ⊆ Subst(K) and X ⊆ ∩ θ∈Θ Dom(θ) we have

Proof.

Conceptual Knowledge

To bridge the gap with [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF] it suffices to construct an inverse system for conceptual knowledge.

Analysis of Predicates of Experience

Let K = (u, S, O, R) be a stable compact cognitive state. Let P (x 1 , . . . , x n ) be a predicate of experience in Obj E (K). there exists an equivalence class Θ P ⊆ Subst(K) and A ⊆ Obs K (Θ P ) such that:

with r∈A Var(r) = {x 1 , . . . , x n }. is also satisfied by σ. However we also note that by construction, if this substitution σ is in Θ P , it satisfies both formulas.

Second, assume now that R ⊆ R, and let A = A ∩ R . Since the valuation of each formula does not change, it is tautological that if a substitution σ satisfies:

Let Θ P be an equivalence class in Subst(K), let A ⊆ Obs K (Θ P ), and let:

r∈A r θ∈Θ P Val u (rθ) Two cases are possible:

• If Θ P is empty, Obs K (∅) = ∅, and thus A = ∅ and m = 0. Thus the conjunction is always true, i.e., P = 1. Any substitution satisfying P (x 1 , . . . , x n ) also satisfies 1;

Technical report No. IRIT/RR-2022-08-FR https://www.irit.fr/ Yannick.Chevalier/ -Yannick.Chevalier@irit.fr

• Otherwise from the above discussion we have that any substitution θ ∈ Θ P satisfies both P (x 1 , . . . , x n ) and P (x 1 , . . . , x m ). Thus again the image of any substitution that satisfies P (x 1 , . . . , x n ) satisfies P (x 1 , . . . , x m ) By construction P (x 1 , . . . , x m ) is a predicate of experience of K . This reasoning applies on all predicate of experience of K, and given that R ⊆ R and Subst(K ) ⊆ Subst(K) one easily obtains Obj E (K ) ⊆ Obj E (K). This case is generalised with functions between any stable compact cognitive states K , K such that K K.

Projections of the Inverse System

Definition 17. (Predication Projection) Let K = (u, S, 0, R), K = (u, S , O , R ) be two stable compact cognitive states with K K. The predicate projection of K into K is denoted ψ K ,K and is the function:

with:

The two first points of next lemma summarizes the discussion of the preceding section. The last point is by construction. Lemma 8. Let K = (u, S, 0, R), K = (u, S , O , R ), K = (u, S , O , R ) be stable compact cognitive states with K K K.

1. ψ K ,K is surjective;

2. For all P ∈ Obj E (K) of arity n, for all a 1 , . . . , a m ∈ O such that there exists a m+1 , . . . , a n in O with |= K P (a 1 , . . . , a n ), we have|= K ψ K ,K (P )(a 1 , . . . , a m ).

ψ

Next lemma enables a similar construction on the domain.

Lemma 9. Let K = (u, S, 0, R), K = (u, S , O , R ) be two stable compact cognitive states with K K, and

Proof. Trivial by Lemma 7 and R ⊆ R.

Thus if the intersection with O of an equivalence class a ∈ O/ ≡ K is not empty, it is a subset of a unique equivalence class a ∈ O / ≡ K . Let h K ,K be provisionally defined as the mapping a

Considering the image of the equivalence class containing each t ∈ O ⊆ O shows that this mapping is surjective. It is extended as follows to Dom(K): Predicate and domain projections are related in the following lemma. The first point is by construction, the second by Lemma 8.

Then the predicate and domain projections of K into K are surjective and

• For all a 1 , . . . , a n ∈ Dom(K) and

• Model homomorphism: for all P ∈ R f there exists a subset m f ≤ n such that

Given a stable cognitive state K = (u, S, O, R) let K ↓ be the set of stable compact cognitive states K = (u , S , O , R ) such that K K and u = u. We have:

is an inverse system of models.

We deviate here from the treatment in [START_REF] Achourioti | A Formalization of Kant's Transcendental Logic[END_REF] to prove that this inverse system of models has a non-empty inverse limit. Given K K ∈ K ↓ define: Definition 20. (Threads of an inverse system of models) Let F be a directed poset and

A Example application: Detection of Network Protocols A.1 Detection of purely parallel processes

While process mining [START_REF] Agrawal | Mining process models from workflow logs[END_REF] usually focuses on the discovery of workflow graphs encoding conditionals and loops, the detection of synchronisation between messages is more often, as e.g., in the case of a protocol, a sequential activity without holes: Messages a and b in an order are always followed by messages c and d, etc. In the case of the CAN Bus these sequences occur in two contexts. In a MFM protocol execution that starts with an initial message, replied to with an ack, and followed by a sequence of messages with a counter. Or in the case of a proper design of the CAN Bus in which such synchronisation is introduced to avoid collisions between messages. These are examples of purely parallel processes [START_REF] Gunawardena | Deducing causal relationships in CCS[END_REF] that are built with sequential and parallel composition only, i.e., with no non-deterministic choice.

Let S be a DXS. A subset S c ⊆ S of terms which are applications of split functions on "X" is called a pre-classification. If it is maximal then it is the classification of the DXS. If the codomain of "X" is the set of possible CAN frames, then the codomain of each t in the classification S c is also the set of CAN frames. We assume that all the events in the log are distinct e.g., by adding a time of capture. To simplify notations we denote e ∈ u if the event e occurs at some position in the word u, and |u| the length of the word u.

Algorithm. Let S be a DXS with a classification set S c . A representation function nb_occ is applied on each t ∈ S c to count the number of occurrences of messages in the interpretation of the term t. The state of the network after seeing a trace u is represented by a boolean square matrixP Sc (u) indexed by terms in S c and defined inductively on traces with:

When analyzing a log Σ u∈U u we let P Σ u∈U u Sc = Σ u∈U P u Sc be the coordinate-wise conjunctions of the matrice P u Sc for u ∈ U . Ordering the matrice with the extension on all coordinates of the ordering on booleans, one easily checks that the conjunction being the sup of boolean values, this function is monotonic and algebraic and thus can be extended by continuity to infinite words.

In the following definition, the semi-colon denotes sequential composition, a set of term denotes a parallel composition of these terms, and the while true do denotes an unbounded iteration of the process. Definition 25. (Purely Parallel Process-PPP Let S be a DXS with a classification set S c . An iterated purely parallel process is a process of the while true do (A 1 ; . . . ; A n ) where A 1 , . . . , A n is a partition of a subset of S c .

A PPP P = while true do (A 1 ; . . . ; A n ) is unambiguous on trace u = (e i ) 1≤i≤N if furthermore for all 1 ≤ i ≤ N if e i occurs in [ [t] ] u and intput for t, t ∈ ∪ n i=1 A i then t = t .

Technical report No. IRIT/RR-2022-08-FR https://www.irit.fr/ Yannick.Chevalier/ -Yannick.Chevalier@irit.fr