Michael Freund
email: micfreund@gmail.com

Ordered models for concept analysis

Keywords: categorization, prototype theory, categorial membership, typicality, deep learning, category-based induction, resemblance theory

In this paper, I propose a simple ordered model for categorization theory. When a concept is grasped through an auxiliary set of features, stemming from a description of the concept or from a resemblance to some typical exemplars, categorial membership, typicality and resemblance can be accounted for by means of weak order relations. These orders render precise the notion of an object 'falling more' than another under this concept, being 'a more typical exemplar' or 'resembling more' this concept. The membership and typicality orders can be naturally extended to compound concepts, without the drawbacks that are classically encountered in conjunction theory. Moreover, these orders reveal themselves to be a particularly adequate tool for the resolution of problems linked with category-based induction.

Introduction

How do we form concepts ? What makes us decide that di↵erent objects may be gathered under a common label ? And once this label has been set, how do we account for its adequacy for new items ? These questions stand at the root of all problems concerning the categorization process. Several models has been proposed since the primitive formalism of Frege [START_REF] Frege | Begri↵sschrift, eine der arithmetischen nachgebildete formelsprache des reinen denkens[END_REF] in which concepts were assimilated with simple one-place predicates. Apart from letting aside the problem of typicality, this view reduced categorization to an all-or-nothing process that only two-valued truth functions could account for. After the work of Eleanor Rosch however, it appeared that categorial membership and typicality should be evaluated by more sophisticated tools: degrees functions [START_REF] Rosch | Cognitive representations of semantic categories[END_REF], membership functions [START_REF] Zadeh | Fuzzy sets[END_REF], geometrical measures [START_REF] Gärdenfors | Conceptual spaces: The geometry of thought[END_REF], or quantum mechanics [START_REF] Aerts | Quantum structure in cognition[END_REF]. In this perspective several models were proposed, all aiming at a unified quantitative theory for categorization.

My approach di↵ers from the preceding ones, in that I consider categorial membership and typicality as comparative notions. As I argued in [START_REF] Freund | On the notion of concept I[END_REF] and [START_REF] Freund | On categorial membership[END_REF], the relative strength with which a concept applies to an object is best accounted for by a (pre)order relation among the objects of the universe. To take an example, an agent may be unable to assign a precise birdhood degree to a bat or to a tortoise, while ready to attribute more birdhood to one of these items than to the other. Similarly, one may consider the duck as a more typical exemplar of a bird than the penguin, without having an idea of what their typical degree could be.

In this framework, every concept endows the agent's universe of discourse with a couple of conceptual orders. The first one, the membership order, compares the strength with which a concept applies to the objects of the universe. It may be seen as a way of comparing objects that do not necessarily fall under the concept. The second one, the typicality order, is meant to compare the relative typicality of the exemplars of the concept. The knowledge of these two orders is equivalent to that of the associated concept: two concepts agree if and only if they have same membership order and same typicality order. hotel plein ciel

The determination of the conceptual orders is not always possible. In [START_REF] Freund | On the notion of concept I[END_REF] and [START_REF] Freund | On the notion of concept II[END_REF], an explicit construction was proposed for concepts that belonged to a specific class -the family of constructible concepts. However, this construction su↵ered from two drawbacks: first, the set of constructible concepts is di cult to circumscribe, as it rests on the di↵erence between sharp and vague concepts. Second, the construction of the membership and the typicality orders required the use of recursively defined degree functions, thus contradicting the philosophy of a supposedly purely comparative theory. The aim of the present paper is to remedy these failures and propose, for a su ciently large family of concepts, a coherent and general theory based on natural conceptual orders, su ciently robust to address the principal problems encountered in categorization theory.

This paper is organized as follows: in Section 2, the di↵erence between concepts and features is evoked and discussed. This leads to the notion of featured concepts, which is central in this paper. A construction of the membership order, based on the defining feature set for simple concepts, is then developed in Section 3. This order gives rise to an auxiliary definition of membership degree. Membership orders and degrees can be extended to the class of compound concepts obtained through the determination operator; this provides an interesting framework for the study of the conjunction e↵ect. Section 4 deals with typicality for simple and compound concepts, while questions linked with resemblance theory are discussed in Section 5. All these notions being settled, it is then possible to tackle some classical problems linked with category-based induction: this is the object of Section 6. .

Featured concepts 2.1 Back to the attributional theory

The classical theory of categorization viewed concepts as theoretical objects that could be defined by a certain number of properties: vertebrates that have beak and feathers were labelled birds, a car could be defined as a road vehicle powered by an engine able to carry a small number of persons, and democracy was a system of government by all the eligible members of a state. In this perspective, where each concept was endowed with a set of attributes, categorization relative to a concept boiled down to categorization relative to its features. This attributional view was advocated by some authors in the late seventies [START_REF] Smith | Structure and process in semantic memory: a featural model for semantic decisions[END_REF] and [START_REF] Smith | Categories and concepts[END_REF]. It gave rise to the so-called binary model, in which two auxiliary sets are attached to a concept. On the one hand, the defining feature set provided the conditions that an item should satisfy in order to fall under a given concept; on the other hand, the characteristic set listed the features that an object should have to be qualified as a typical instance of this concept. Given for instance the concept to-be-a-fruit, one may take as defining feature set the set consisting of the two elements to-be-a-vegetable and to-heave-seeds, while the characteristic set would include features like to-grow-on-trees, to-be-sweet, to-be-raw-edible, to-yield-juice.

The attributional theory was thereafter rejected by most researchers, as it appeared that concepts defined by a conjunction of features formed an exceptional subclass. Fodor for instance [START_REF] Fodor | Concepts: where cognitive science went wrong[END_REF] argued that there exists practically no examples of successful definition around. Without being so radical, it is clear that a great deal of concepts are deprived of any set of defining features: what list of attributes could be attached for concepts like to-be-a-citrus fruit, to-be-a-lie, or to-be-a-heap ? However, in spite of this, it appears that the attributional view is justified for certain well-defined families of concepts: such is for instance the case for most nominal concepts, i.e. concepts that are conventionally defined, like to-be-a-mammal, to-be-a-theft or to-be-a-refugee. In particular, this remains true for scientific concepts, like to-be-a-vortex or to-be-a-square. Furthermore, it may happen that a concept, first grasped through its exemplars, is thereafter sharpened with the help of a set of defining features: thus, the concept to-be-a-bird, a natural kind concept, was revisited by naturalists and turned into the pseudo-nominal tohave-feathers + to-have-a-beak + to-have-wings. Note also that even for nondefinable concepts, class membership may still depend on auxiliary features: this is the case when categorial membership is induced through resemblance to a prototypical exemplar. Then, it is the features of this prototype that play the role of defining features.

These considerations show that the family of attributional concepts is large enough to deserve a treatment of its own. Since attributional concepts can be studied with the help of quite elementary mathematical tools -contrary to the examples evoked in the preceding paragraph -there is no reason not to devote to them a special study. Such is the aim of the present paper.

It is necessary to emphasize at this point that this study does not aim at providing an objective model for categorization, even for the restricted area of attributional concepts. Indeed, the defining feature set and the characteristic set on which this construction is based are by no means well-defined. They vary from an agent to another and, for a given agent, they may change with time. It may even happen that a concept is seen as attributional by an agent, while deprived of this quality by another one. It should be therefore understood that the model proposed in this paper is meant to reflect, at a given precise time, the single point of view of a subjective particular agent.

Concepts and features

The terms concept and feature cover di↵erent notions. Formally, concepts are most often introduced through the auxiliary to-be, followed by a noun: to-bea-bird, to-be-a-vector-space, to-be-a-democracy. Features may be presented through a verb (to-fly), the auxiliary to-have, followed by a noun (to-havea-beak), or the auxiliary to-be, followed by an adjective (to-be-tall ). While concepts appear as unary predicates, this condition is no more necessary for features. Features, like concepts, apply to the objects at hand but, contrary to concepts, they are context-sensitive: they borrow part of their significance from the concept they are attached to. Properties like to-be-tall, to-be-rich or to-be-red take their full meaning only in a given context, that is when qualifying a well-defined entity. Even simple verbal forms like to-fly, torun, to-live-in-water, to-be-made-of-metal need a principal referent concept to fully seize the strength with which they apply to di↵erent items. Thus, the concept a feature applies to may be seen itself as a contextual determination of this feature. To summarize, the meaning of a feature depends on the context in which this feature is used, contrary to the meaning of a concept, which exists by itself.

It does not seem at this stage that any formalism can fully account for the di↵erence between features and concepts. It is true that in Description Logics, a di↵erent treatment is applied for one and two-places predicates: binary predicates characterize indeed the roles of the language, which are used to express relationship between the concepts [START_REF] Nardi | An introduction to description logics[END_REF]. In this famework, to-be-a-tree will be a concept, expressible by a single symbol A, but to-have-green-leaves is a role, expressed by a formula of the type '8 hasLeaves.Green'. However, no di↵erence is made in Description Logics between the unary predicates that translate a notion of concept and those that translate a notion of feature.

It should be noted that, when considering a feature f of a concept ↵, the way f applies to an object is generally itself related to the categorial membership of an auxiliary concept . Consider for instance the feature to-have-wings. In order to evaluate to which degree this feature applies to an item x, we must be able to determine what exactly covers the concept to-be-a-wing, and which objects fall under it (for a discussion on the di↵erence between knowing what an X is and knowing what it is to have an X, see [START_REF] Fodor | Concepts: where cognitive science went wrong[END_REF]. This observation shows that circularity cannot be avoided when trying to build a general mathematical model for categorial member-ship. However, such is not the purpose of this work, which aims at analyzing how the knowledge of a concept can be drawn from the knowledge of its associated set of features, without questioning the nature and the sources of the latter.

Applicability functions and applicability orders for concept features

The strength with which a feature f of a concept ↵ applies to an object is usually measured in a given ontology through a percentage or an applicability degree function ↵ f that takes its values in the unit interval. Concerning the range of this function, it is important to observe that it can be most often circumscribed to a finite subset of [0, 1]: this is clearly true for fuzzy features like to-be-tall, to-be-rich or to-be-warm, since the measure of their applicability is always approximative (to an inch, a cent or a degree). On the Brittany coast of France, for instance, the set of water temperatures t in July ranges for from 15 to to 25 degrees Celsius degrees, thus covering 11 possible (integral) values. In this context, the function associated with the concept warm may be given by ↵ f = t/10 1.5. The finiteness of the range of ↵ f is even more obvious in the general process of categorization: ranking the objects relatively to a feature of a given concept only yields a small number of equivalence classes. To determine, for instance, to which extent a flower may be considered as a poppy, one roughly evaluates its redness, its shape and the size of its petals. Concerning the redness, comparison with other objects shows that only a finite number of discernible reds separate the color of that particular flower from that of an ideal poppy. Thus, in the context of a to-be-a-poppy, there exists only a small number of possible degrees of redness. The same observation can be made concerning the other features that define or describe poppies, like the shape and the size of the petals.

For this reason, this paper will be devoted to the family of concepts whose features can be weighed on a finite scale. These concepts form the family of featured concepts. Given a featured concept ↵, the way any of its associated feature f applies to an item is accounted for by an applicability degree function ↵ f that takes only a finite number of values. Equivalently, we may say that f , as an ↵-feature, generates an applicability order ↵ f defined for any objects x, y of the universe of discourse by:

x ↵ f y if and if ↵ f (x)  ↵ f (y).
The relation thus defined is a total order that has only finitely many equivalence classes. There exists therefore only a finite number of intermediate states between an object x totally deprived of f and an object y to which the feature f fully applies.

Apart from the finiteness condition, featured concepts will be required to satisfy an agreement condition to guarantee the existence of at least an object to which simultaneously apply all the defining and characteristic features associated with a concept ↵.

This leads to the following definition:

A featured concept ↵ is a concept for which there exists a finite set of defining features (↵) and a finite set of characteristic features ⌅(↵) that satisfy the two properties :

1. for every defining or characteristic feature f , the corresponding applicability function ↵ f takes a finite number of values 2. There exists at least an item z such that ↵ f (z) = 1 for all defining or characteristic features f . As was recalled in paragraph 2.1, in the agent's mind the set (↵) is constituted by attributes that appear to be essential for the concept realization: the only objects to which ↵ applies are those that possess these attributes. On the contrary, the characteristic features are only present in the typical exemplars of the concept.

The family of featured concepts will be denoted by F. In order to lighten the notations, the superscript of the applicability functions and degrees will be omitted, so that f and f stands for ↵ f , and ↵ f . However, it is necessary to keep in mind that the applicability order or the applicability function of a feature is always defined relatively to the concept it qualifies.

Membership orders

In general, the human mind has no tool at its disposal to directly evaluate the categorial membership of an object: in the extremal cases, we may be able to decide that a given object is or is not a member of the concerned category, but we do not know in the intermediate states how to quantify its partial membership: a conventional bomb is definitely not a weapon-ofmass-destruction (WMD), and the same is true for a machine gun, yet, we are unable to attribute a precise degree of membership to any of these items taken alone. We can only compare them. Similarly, we are unable to assign a precise membership degree to a sink as a piece of furniture, while being ready to admit that it is 'more' a piece of furniture than a heat-pipe, and 'less' a piece of furniture than a window.

As a matter of fact, concerning membership evaluation, and apart from the binary distinction between members and non-members of a category, the best thing the human mind seems to be capable of is to compare two objects and decide which one, if any, falls 'more' under the concerned concept. Thus, the concept to-be-a-weapon-of-mass-destruction will be generally considered as applying more to a machine-gun than to an arquebus, and less to a spear than to an arquebus. Clearly, this judgement shows the existence of a basic ordering induced by the concept to-be-a-weapon-of-mass-destruction in the universe of discourse. This ordering is by no means a consequence of a supposed degree assignment that the agent has set a-priori on the objects at her disposal: if directly questioned what membership degree should be attributed to a machine-gun considered as a WMD, an agent will be generally unable to provide a sensible answer. Of course, such an assignment may be established once comparison has been made between the items at hand. For instance, a non-decreasing ranking like bludgeon  sword  crossbow  arquebus  gun  machine-gun  flamethrower  conventional bomb  scud  atomic bomb may yield a posteriori a membership degree of the concerned items, which can be readily visualized from their position on a [0,1] scale: thus, an atomic bomb will be considered as being 100% a WMD, a scud as 90%, a conventional bomb as 80% and so on. The point is that these numerical values will appear as a consequence of a pre-recognized order among the di↵erent weapons that are part of the agent's universe: they will not be at the origin of it. This construction of a membership degree as a secondary tool, stemming from a membership order, will be examined in details in section 3.3.

Order relations therefore appear to provide the most adequate model to account for categorial membership as perceived by a cognitive agent. Appealing systematically to relations of this type whenever it is possible avoids the drawbacks that may result from the application of more sophisticated theories. It is true that in some cases, order relations may be insu cient to fully treat categorial membership -this will be for instance the case for fuzzy concepts, or for vague concepts of a continuous type. However, concerning the specific class of featured concepts, the tool provided by weak order relations is su ciently powerful to fully address the categorization problem.

In this perspective, the fact that a concept ↵ may apply more (or better ) to an item x than to an item y will be translated by a preorder (reflexive and transitive) relation on the set O of objects, real or imaginary, that are part of the agent's universe of discourse. This relation will be denoted by µ ↵ . The expression 'x µ ↵ y' therefore translates the sentence 'the concept ↵ applies at least as much to the object y as to the object x'.

The corresponding strict partial order will be denoted by µ ↵ , that is x µ ↵ y if and only if x µ ↵ y and not y ↵ x. In the general case, and contrary to most of the existing theories, the relation µ ↵ will not be supposed to be total. There is no reason indeed to a priori eliminate the case where the membership of two objects is incomparable. Taking again the bird example, this enables us for instance to deal with the case where an agent refuses to compare the birdhood of a bat with that of a tortoise.

The case of featured concepts

Let now ↵ be a featured concept and suppose that its defining feature set (↵) consists of the k features f 1 , f 2 , . . . , f k . In the perspective of the attributional view, the applicability orders f 1 , f 2 , . . . , f k induced on O by these features are part of the agent's knowledge. The assumption that the knowledge of the features is su cient to acquire knowledge of the target concept requires that the membership order µ ↵ should naturally stem from the f 1 , f 2 , . . . , f k . One could then simply consider that µ ↵ is the intersection of the 0 f i s, but this would ignore the internal structure of the set (↵). Indeed, the defining features of ↵ cannot be considered as equivalent. In the agent's mind they do not necessarily weigh the same weight. For instance, a particular agent may associate with the concept to-be-a-bird the defining set {to-be-a-vertebrate, to-be-oviparous, to-have-feathers, to-have-a-beak, tohave-wings}, and consider moreover that having wings is a more important feature for birdhood than having a beak. For this agent consequently, a bat will be given more birdhood than a tortoise. To account for this phenomenon, it is necessary to equip the set (↵) with a salience relation, which will be simply translated by a strict partial order > (↵) .

The membership order induced by ↵ can be now defined by:

x µ ↵ y i↵ for each defining feature f i such that y f i x, there exists a defining feature f j , f j > (↵) f i , such that x f j y. Thus, the concept ↵ applies at least as much to y as to x if each of its defining feature that applies more to x than to y is dominated by a defining feature that applies more to y than to x (see [START_REF] Freund | On categorial membership[END_REF] for a justification of this construction).

The relation µ ↵ sets a partial (weak) order on the set O. Its associated strict partial order reads x µ ↵ y if and only if x µ ↵ y and there exists some defining feature f i for which x f i y. Example 1 Let ↵ be the concept to-be-a-bird, and suppose that, from the point of view of an agent, its defining feature set in the context of living beings is the set {to-have-two-legs, to-lay-eggs, to-have-a-beak, to-have-wings} with the following salience order: to-have-a-beak > s to-lay-eggs > s to-havetwo-legs, and to-have wings > s to-lay-eggs> s to-have-two-legs. Suppose for the sake of simplicity that, in the agent's mind, membership to any of these features is a two-valued function. Let s, m, t, b and d respectively stand for a sparrow, a mouse, a tortoise, a bat and a dragonfly. Then the induced membership order is determined by the following arrow : ↵ d, since the concept to-have-two-legs under which the bat falls, contrary to the dragonfly, is dominated by the concept to-lay-eggs that applies to the dragonfly and not to the bat. On the other hand, one does not have d µ ↵ b, as nothing compensates the fact that the dragonfly lays eggs and the bat does not. This yields b µ ↵ d. Note also that the tortoise and the bat are incomparable: one has neither b µ ↵ t, nor t µ ↵ b. The strict ↵-membership order therefore reads:

two
m b d t s ⇢ ⇢ c c c c c c    

Essence and Extension

The membership order µ ↵ adequately translates the notion of membership to a category. Indeed it follows from the agreement condition that there exist µ ↵ -maximal elements in O, namely those that fall under all the defining features of ↵. These objects form the extension, or the category, of the concept ↵, denoted by Ext ↵. Its elements constitute the exemplars, or the instances, of the concept.

This definition by means of maximal membership conforms with the intuition: an object x (fully) falls under a concept ↵ if ↵ cannot apply more to an object y than to x. Whatever salience order is set on (↵), an object falls under the featured concept ↵ if and only if it falls under each of its defining features. In other words one has Ext ↵ = T (Ext k) k2 (↵) . One retrieves here the classical characterization of a defining feature set as a set of features that are 'individually necessary and jointly su cient to ensure membership relative to ↵'.

As mentioned above, the set (↵) has no objective character: it consists of the features that a given agent would choose as most suitable to define the extensional aspect of a concept. Another agent may choose a di↵erent defining feature set 0 (↵), even if both agents agree on the definition of ↵. The set Ext ↵ provides a more objective representation of ↵: if two agents agree on ↵, they will agree on Ext ↵. More generally, the role played by the defining feature set may be extended to a larger set, Ess ↵, called the essence of ↵. This set gathers the concepts and features that apply to every element of Ext ↵, that is:

Ess ↵ = { 2 F; Ext ↵ ✓ Ext }.
One may consider the elements of this set as the essential attributes of the concept. It readily follows from the definitions that the extension of ↵ can be retrieved from its essence: one has indeed Ext ↵ = T (Ext k) k2Ess ↵ . In the language or Formal Concept Analysis, this shows that the pair (Ext ↵, Ess ↵) can be considered as a formal concept in the context (O, F, I), where (x, ↵) 2 I i↵

x falls under ↵.

The notion of subconcept can be now precisely defined : a concept will be said to be a subconcept of ↵ i↵ µ ✓ µ ↵ . This implies in particular Ext ✓ Ext ↵, and consequently Ess ↵ ✓ Ess .

Two remarks have to be made concerning the above definitions. First, the essence of a concept as defined above corresponds to the classical one (see [START_REF] Desclés | Logic of determination of objects: How to articulate 'extension' with 'intension' and 'objects' with 'concepts[END_REF])), provided one remembers that the universe of discourse includes imaginary, as well as real, objects. Restricting the set O to real objects would indeed lead to counterintuitive results: for instance consider the concept to-be-US-president, and suppose that it is known that all past and present US presidents were golf players. Then the attribute to-be-agolf-player applies to all instances of to-be-US-president; if only real existing objects were considered, the feature to-be-a-golf-player would become part of the essence of to-be-US-president...! Enlarging the set of real objects to imaginary ones avoids this drawback, because we can imagine an US president that does not play golf.

Another remark is that the essence of a concept, as defined above, gathers two di↵erent families of concepts. On the one hand, we find the specific attributes that are attached to this concept and help distinguishing it from neighboring concepts. In the example of to-be-US-president, such is for instance the case of the concepts to-sleep-in-the White-House, to-convene-Congress, to-command-the-US-armed-forces -in the current literature, this set is usually referred to as the 'Intension' of the concept. On the other hand, we have the generic attributes, which the concept has inherited from some super-concept: for instance, the generic attributes of the concept to-be-USpresident include the features to-be-mortal, to-be-a-vertebrate or to-have-aheart, which are part of the essence of to-be-a-man.

The distinction between specific and non specific features plays an important role in category-based induction. It will be more precisely studied in section 6.2.2.

Membership distance and membership degree

Since µ ↵ is generally not a total order, there exists no membership degree function ↵ that would satisfy

x µ ↵ y i↵ ↵ (x)  ↵ (y).
It is however possible to approximate the notion of membership degree by considering increasing chains of objects, similarly to what was evoked in the WMD example. The following construction stems from the fact that any strictly increasing chain

of the form x 1 µ ↵ x 2 µ ↵ . . . µ ↵ x k µ ↵ .
. . must be of finite bounded length (this because of the finite number of defining features, together with the finiteness condition of paragraph 2.3). Given an object x, it therefore makes sense to consider the maximal length of a chain

x µ ↵ x 1 µ ↵ . . . µ ↵ x n with last term x n 2 Ext ↵.
(m) = 0, µ ↵ (b) = 1/2, µ ↵ (t) = µ ↵ (d) = 3/4) and µ ↵ (s) = 1.
3.4 Categorial membership for compound concepts

The determination connective

It is sometimes possible to determine a concept ↵ by another concept . We obtain in this way a compound concept, which will be denoted by ? ↵. This determination is most often realized by the combination of an adjective or an adjectived verb with a noun, like in the compositions to-be-a-carnivorousanimal, to-be-a-flying-bird, to-be-a-french-student, to-be-a-red-apple. It can also take the form of a noun-noun combination, like in to-be-a-pet-fish, to-bea-barnyard-bird, and, more generally, of a relative clause that will be globally encapsulated by the concept (e.g. to-be-an-American-who-lives-in-Paris).

Typically, the concept becomes a simple feature of the compound concept ? ↵. Its role can be therefore considered as secondary, compared with that played by the principal concept ↵: to-be-red is a feature of the composed concept to-be-a-red-car, and to-be-a-woman becomes a feature of a to-bephysician-that-is-a-woman.

Not to mention the simple conjunction (to-be-an-history-teacher & to-bea-geography-teacher ), which provides equal importance to both constituents, other types of connective exist in which the principal role is attributed to the modifier, like in to-be-a-Picasso-painting. These will not be studied in the present paper.

As a last remark, it is important to keep in mind that only the intersective conceptual combinations are accounted for: the objects that fall under the composed concept ?↵ are exactly the ones that both fall under ↵ and under (see [START_REF] Kamp | Prototype theory and compositionality[END_REF] for the distinction between intersective and non-intersective modifiers). This shows that the determination connective ? is only a partial operator: given arbitrary ↵ and , it may be meaningless to build the concept ? ↵. For instance, there is no sense in talking of a sailing-number or a wooden-salience. Such pseudo-concepts correspond to nothing, and no object, real or fictitious, can be thought of falling under them, contrary to imaginary concepts like a pink-elephant, a striped-apple or a flying-cow : these latter definitely have a non-empty extension, because we can imagine a pink elephant, a striped apple or a flying cow.

Similarly, concepts determined through qualitative or quantitative adjectives, like a big-piano, or a nice-house will not be taken in consideration, as one cannot consider that to-be-big or to-be-nice are well-defined concepts. When forming the composition ? ↵, it is always understood that the intersection Ext ↵ \ Ext is a non-empty well-defined set.

Membership orders for compound concepts

Let ↵ and be two concepts for which corresponding membership orders have been defined, and suppose that the determination of ↵ by is meaningful, that is Ext ↵\Ext 6 = ;. We want to set a membership order on the concept ?↵ that gives preeminence to ↵ over . This can be simply done by setting:

x µ ?↵ y if x µ ↵ y and, either x µ ↵ y, or x µ y. In this framework, the concept to-be-a-flying-bird will be considered as applying more to a penguin than to a bat: indeed, the principal concept is that of being-a-bird, while to-fly appears as a simple feature, less important than the concept it modifies.

The relation thus defined is reflexive and transitive. Since it is clearly a subrelation of µ ↵ , it makes ? ↵ a subconcept of ↵. The hypothesis that Ext ↵ \ Ext 6 = ; implies that full categorial membership can be recovered through the µ ?↵ -maximal elements. If we define indeed the extension Ext ( ?↵) of ?↵ as the set of µ ?↵ -maximal elements, it holds Ext ( ? ↵) = Ext ↵ \ Ext . Categorial membership is therefore compositional : an object falls under a determined concept if and only if it falls both under the concept and under its determiner. The category of red-cars exactly covers all the items that are red and that are cars. Compositionality for µ ?↵ -maximal elements does not extend to arbitrary items: an object y may fall more than an object x under ? ↵, while falling less than x under : to-be-a-flying-bird for instance applies more to a penguin than to a bat, although to-fly applies more to a bat than to a penguin.

Membership degree and the conjunction e↵ect

As was done for simple concepts, a membership distance can be defined for compound concepts of the form ? ↵: for any object x, let µ ?↵ (x) denote the length of a maximal µ ?↵ -chain starting from x and ending in Ext ( ? ↵). Note that µ ↵ (x)  µ ?↵ (x). If N ?↵ is the length of a maximal µ ?↵ -chain in O, the ( ? ↵)-membership degree of x may be then defined by

µ ?↵ (x) = 1 µ ?↵ (x)
N ?↵ . An interesting side-e↵ect of this construction is that it renders possible a modelling of the so called conjunction e↵ect. This phenomenon was observed in 1981 by [START_REF] Osherson | On the adequacy of prototype theory as a theory of concepts[END_REF]. It has been since at the origin of numerous research and experiments (see in particular [START_REF] Hampton | Overextension of conjunctive e↵ects: Evidence for a unitary model of concept typicality and class inclusion[END_REF], [START_REF] Tversky | Features of similarity[END_REF], [START_REF] Kamp | Prototype theory and compositionality[END_REF], [START_REF] Aerts | Quantum structure in cognition[END_REF], [START_REF] Franco | The conjunction fallacy and interference e↵ects[END_REF], or [START_REF] Hampton | Compositionality and concepts[END_REF] for a general review. The conjunction e↵ect can be described by the fact that an item may be found to be more strongly a member of the conjunction of two concepts than a member of one of them. Thus, a guppy appears to be more a member of the concept to-be-apet-fish than a member of to-be-a-pet or to-be-a-fish. This problem is di↵erent from the one evoked at the end of the preceding section: here, one does not compare the membership of two objects relative to a single concept, but the membership of one object relative to two concepts. The use of membership degrees renders possible an explanation of the conjunction e↵ect. It turns out indeed that nothing stands against the fact that the ( ? ↵)-membership degree of an item might be greater than its ↵-membership degree, as can be seen in the following example:

Example 3 Let us take again the degree computations of example 2. The chain m µ ↵ k µ ↵ b µ ↵ d µ ↵ s being supposed to be maximal, one has µ ↵ (k) = 1/4. If is the feature to-be-black, equipped with a two-valued membership degree function, one may think of a maximal ? ↵-chain like

m µ ?↵ m 0 µ ?↵ k 0 µ ?↵ k µ ?↵ b µ ?↵ b 0 µ ?↵ d µ ?↵ d 0 µ ?↵ s µ ?↵ r
, with m: a white mouse; m 0 : a black cat; k 0 : a (red-brown) kangaroo; k: a black macaque; b: a brown bat; b 0 : a black bat; d: a blue dragonfly; d 0 : a black fly; s: a sparrow; r: a raven. This leads to N ?↵ = 9, and µ ?↵ (k) = 1/3, showing that, in this model, the macaque is more a black bird than a bird.

Objections to the compositional theory

Several arguments have been developed against a theory of compositionality in which membership to a compound concept simply boils down to membership to each of its constituents. It has been objected for instance that there is a di↵erence between the concept s ? g (being-a-game-that-is-a-sport and the concept g ? s (being-a-sport-that-is-a-game), and that they do not have the same exemplars, although, in the proposed model, the concepts s?g and g ? s would have the same extension. But even though they share the same exemplars, these concepts are not equal, as they have di↵erent membership orders. Moreover, although some experiments seem to contradict this assumption, an item which is considered as a sport that is a game must be both a sport and a game -even if it is before all considered as a sport. Confusion comes when one mixes membership and typicality, as is the case of the unary model, where a unique scale is used to measure these two notions. Things would be of course di↵erent if we considered a composed concept like 'to-be-a-sport-that-is-secondarily-a-game'. Nevertheless, such a complex concept cannot be accounted for through the determination connective ? the way it has been circumscribed.

Another example that would tend to reject compositionality is provided by the composed concept to-be-school-furniture. Experiments show that people consider a blackboard as a clear exemplar of this concept, although not an exemplar of the unmodified to-be-furniture. The explanation is that here again the compound resulting concept is not really obtained through the determination connective ?, the same way to-be-a-urban-furniture is not a determination of to-be-a-furniture. Indeed, by default, to-be-a-furniture refers to to-be-home-furniture, and school-furniture is not home-furniture that can be found in school. This shows that rather than a determination, the operation that yields school-furniture from furniture is a modification. Clearly there is no contradiction in the fact that an instance of a modified concept is not an instance of the unmodified concept.

It is interesting to note that the compound concept to-be-school-furniture cannot be translated in French through a determination or a modification of the words meubles or ameublement, which are used for usual (home) furniture. The French word that translates the furniture dedicated to some specific use is mobilier : one speaks then of mobilier d'école (school-funiture), mobilier urbain (urban-furniture), or mobilier de bureau (o ce furniture). The compound concept obtained in this way is fully compositional.

Typicality

The relative typicality of objects falling under a concept ↵ is accounted for through an order relation that stems from the characteristic set associated with ↵. This set consists of features that, from the point of view of an agent, are su cient to characterize the typical exemplars of ↵. For instance, if ↵ is the concept to-be-a-bird, the associated characteristic set ⌅(↵) may include the concepts to-fly, to-sing, to-live-in-the-trees. It may also include attributes that are related to the average size, the shape or the weight of the concept typical exemplars, like to-be-small or to-be-light. On the contrary, concepts like to-have-feathers and to-have-wings, which apply to all instances of ↵, will not be part of the characteristic feature set, but they may figure in the defining feature set (↵).

As was the case for the defining feature set, the characteristic set is supposed to be equipped with a partial salience order, denoted > ⌅(↵) . This order is meant to compare the relative importance of the di↵erent characteristic features.

The typicality order

Let ↵ be a featured concept. For two elements x and y of Ext ↵, we set x ⌧ ↵ y i↵ for each characteristic feature f of ↵ such that y f x, there exists a characteristic feature g, g > ⌅(↵) f , such that x g y. It is easily seen that this relation is a (weak) partial order on Ext ↵. The set of ⌧ ↵ -maximal elements of Ext ↵ will be denoted by T yp ↵. It gathers the typical exemplars of the concept. Clearly, an exemplar z of ↵ is ↵-typical if and only if it falls under all the characteristic features of ↵. It follows that

T yp ↵ = T (Ext k) k2⌃(↵)
. It is possible to parallel the construction proposed in paragraph 3.2, and define the intension of the concept ↵ as the set of concepts and features that apply to every element of T yp ↵. One has therefore Int ↵ = { 2 F; T yp ↵ ✓ Ext }. This set can be substituted to the (subjective) characteristic set used for the definition of T yp ↵. Conversely, it holds

T yp ↵ = T (Ext k) k2Int ↵ . This shows that (T yp ↵, Int ↵) is a formal subconcept of (Ext ↵, Ess ↵).
The intension of a concept includes its essence; the elements of Int ↵ that are not in Ess ↵ are the typical attributes of the concept: they consist of the attributes that are generally but not always true of the exemplars of the concept. They apply to every typical instance of the concept, without applying to all of its exemplars.

Contrary to categorial membership, typicality is not preserved by embedding: typical ostriches are not typical birds. A subconcept of ↵ will be said to be smooth if its typical instances are typical for ↵, that is if T yp ✓ T yp ↵. The concept to-be-a-robin for instance may be seen as a smooth subconcept of to-be-a-bird.

Membership and typicality orders fully determine a concept as they describe how the universe of discourse is structured relative to this concept. Two concepts ↵ and will be considered are equivalent, written ↵ ⌘ , if µ ↵ = µ and ⌧ ↵ = ⌧ . Note that two concepts may have same extension and same typical elements without being equivalent. For instance, such will be the case if their respective defining set and characteristic sets are identical, but equipped with di↵erent corresponding salience orders. The concepts ↵ and will be said to be similar, written ↵ ' , if they have same extension and same set of typical elements

The case of compound concepts

Let ? ↵ be the determination of ↵ by a concept , and define the typicality order ⌧ ?↵ on the set Ext ↵ \ Ext by:

x ⌧ ?↵ y if x ⌧ ↵ y and either x ⌧ ↵ y, or x ⌧ y. This relation is reflexive and transitive. Because of the finiteness of ⌅(↵), the set of ⌧ ?↵ -maximal elements of Ext ( ? ↵) is not empty. This set will be denoted by T yp( ? ↵), and its elements referred to as the typcal instances of ? ↵.

As was the case for membership, the typicality order for composed concept gives preeminence to the initial concept: a typical exemplar of ? ↵ has maximal ↵-typicality among the elements of Ext ( ? ↵). Taking this side however leads to seemingly paradoxical results. It has been objected for instance that this construction makes a gull a more typical exemplar of Antarctic-bird than a penguin, while, for most people, the penguin appears to be the typical Antarctic bird, The explanation is that there is a mix-up between a typical Antarctic bird and a bird that typically lives in Antarctic, this latter being usually interpreted as a bird that mainly lives in Antarctic. Such is indeed the case for the penguin, which, contrary to the gull, is an Antarctic endemic bird. Moreover, the penguin's features are so di↵erent from those of a familiar European birds that they may appear as 'typical' of this atypical species. Typicality indeed is often understood as a di↵erentiation tool: the most typical exemplars of an atypical subcategory tend to be chosen among the less typical exemplars of this category... This interpretation however does not correspond to the usual definition of typicality by means of characteristic features. It covers a di↵erent notion, that accounts for representativeness rather than typicality. To precisely define this notion, it would be necessary to introduce a representativeness order inside a subcategory: for instance, given two exemplars x, y of a subconcept of ↵, one may say that, relatively to ↵, y is a better representative of than x if y is both more -typical and less ↵-typical than x. It is this order relation, di↵erent from typicality, that would render the penguin more representative as an Antarctic bird than the skua or the petrel.

Contrary to membership, typicality is not compositional. The typical instances of ? ↵ cannot be retrieved from the typical instances of ↵ and . This comes from the fact that the set T yp ↵ \ T yp may be empty, like in the example (to-be-an-ostrich)?(to-be-a-bird ). However it is not di cult to see that if the set T yp \ T yp ↵ is not empty, one has T yp \ T yp ↵ = T yp ( ? ↵): a typical black olive is a typical olive that is typically black.

Concerning the determination connective, two interesting properties deserve to be mentioned. The first one is associativity: for any concepts ↵, , , one has ? ( ? ↵) ⌘ ( ? ) ? ↵. Indeed, a straightforward computation shows that the membership and the typicality orders of ? ( ? ↵) and ( ? ) ? ↵ are identical.

The second property is that of idempotence: for any concept ↵, it holds:

↵ ? ↵ ⌘ ↵.
There is no di↵erence between to-be-a-bird-that-is-a-bird and to-be-a-bird.

On resemblance

The notion of resemblance is an important one in the categorization process. It has been at the center of numerous theoretical and experimental studies. Searchers tried to precisely circumscribe this notion, either by defining a resemblance degree between two items, or by determining the link between resemblance, membership and typicality [START_REF] Rosch | Cognitive representations of semantic categories[END_REF], [START_REF] Tversky | Extension versus intuitive reasoning: The conjunction fallacy in probability judgement[END_REF]) and [START_REF] Wittgenstein | Philosophical investigations[END_REF].

Resemblance may be considered as a binary relation between objects (Henry resembles his brother ), between concepts (the wolf resembles a dog), or between an object and a concept (this picture resembles a Picasso). To study this notion first requires to determine which type of resemblance one is dealing with. In this paper, only resemblance between objects and concepts or between concepts will be studied.

Resemblance between objects and concepts

In a first approximation, resemblance between an object and a concept seems to be directly linked with categorial membership : saying that this piece of music resembles Beethoven means that what is heard is close of falling under the concept to-be-Beethoven's work. However, it is clear that resemblance relative to a concept is first perceived as resemblance with the typical instances of this concept. The Beethoven referred to in the preceding example is not the 'young Beethoven', whose compositions still reflect Haydn influence, but the later Beethoven of the second or third period. Similarly, saying that 'Peter's bedroom looks like a boat cabin' refers to a typical boat cabin, excluding for instance a destroyer's cabin... It follows that, when an agent asserts that a particular item x resembles a concept ↵, one may infer, first, that x is not known by the agent to be an instance of ↵, and, secondly that, for this agent, x resembles a typical exemplar of this concept, sharing with it a certain amount of typical attributes.

Thus, looking at a bat, one may say it resembles a bird, just because it has wings, it flies, and it has the size or the shape of a bird. Conversely, an animal may be declared not to resemble a bird if it does not resemble a typical bird, even though this animal is known to be a bird. For instance, looking at a penguin, an assertion like 'this animal does not resemble a bird' is perfectly understandable. Resemblance first deals with the typical attributes of a concept.

In the framework of featured concepts, it seems that resemblance to a concept may be analyzed and treated through a preorder relation in a way similar to what was done for membership and typicality.

The simplest way to do so would be to define on the set (↵) [ ⌅(↵) a salience order stemming from the salience orders of (↵) and ⌅(↵), and then build on O a weak order relation, as was done for membership or typicality. However, in such a model, resemblance would be very much dependent on salience, leading to counterintuitive results: a single ↵-feature with maximal salience, that applied to x and not to y, would make x more ↵-resemblant than y, even though many other ↵-features may apply to y and not to x. To take an example, suppose that ↵ is the concept to-be-a-bird and that to-fly has maximal salience in (↵) [ ⌅(↵). Then bird-resemblance will principally rest on the ability of an item to fly; consequently, bats will be more birdresemblant than kiwis, although having feathers, singing and building nests, taken together, should, at least, compensate the fact that kiwis do not fly.

The following construction seems to remedy this drawback, as it takes into account the number of ↵-attributes that apply to an object x as well as the preeminence of the characteristic features over the defining ones.

Denote by ⇧(↵) the set (↵) [ ⌅(↵) -this set is referred to as the stereotypical set of ↵ (see [START_REF] Connolly | Why stereotypes don't even make good defaults[END_REF], [START_REF] Fodor | Concepts: a potboiler[END_REF], or [START_REF] Jönsson | On prototypes as defaults (comment on connolly, fodor, gleitman and gleitman[END_REF]).

Recalling that (↵) and ⌅(↵) are supposed to be disjoint sets, let > ⇧(↵) be the salience order on ⇧(↵) that extends the salience orders > (↵) and > ⌅(↵) , and satisfies moreover f > ⇧(↵) g for all f 2 ⌅(↵) and g 2 (↵). The study of the ordered set (⇧(↵), > ⇧(↵) ) may be seen as providing a bridge between the binary model and the unary model.

Given an element f of ⇧(↵), define the salience degree of f as the number

s f = 1 + |{h 2 ⇧(↵); f > ⇧(↵) h}|.
Using the f -applicability function f (x) defined in 2.3 renders possible the definition of the ↵-resemblance degree of an element x of O by setting:

⇢ ↵ (x) = ⌃ f 2 ⇧(↵) s f f (x) ⌃ f 2⇧(↵) s f .
The elements of O that are maximally resemblant to a concept ↵ are the typical instances of ↵. Their resemblance degree is equal to 1.

Example 4 Taking again the bird example, suppose that the defining feature set is as in example 1, that is (↵) ={to-have-two-legs, to-lay-eggs, tohave-a-beak, to-have-wings} with salience order to-have-a-beak > s to-layeggs > s to-have-two-legs, and to-have wings > s to-lay-eggs> s to-have-twolegs. Suppose that its characteristic set consists of the three features to-buildnests, to-sing, and to-fly, equipped with the order to-fly> s to-build-nests and to-fly> s to-sing. Computing the bird-resemblance degrees of a bat b, a penguin p and a kiwi k yields ⇢ ↵ (b) = 11/26, ⇢ ↵ (p) = 9/26 and ⇢ ↵ (k) = 19/26. The bat is less bird-resemblant than the kiwi, but more bird-resemblant than the penguin.

Note that, in this model, categorial membership cannot be directly retrieved through resemblance: there exists no degree threshold above which an item can be declared to be an exemplar of the target concept. All what can be said, is that an item with ↵ resemblance degree equal to 1 must be a typical instance of ↵. This comes from the fact that, in evaluating resemblance, one compares objects with the typical instances of a concept, rather than to arbitrary exemplars of this concept.

Resemblance between concepts

One may again interpret concept resemblance as resemblance between typical instances : judging that 'Braque resembles Picasso' amounts to say that a typical painting of Braque resembles a Picasso. In other words, one will say that a concept ↵ resembles a concept if every typical instance of ↵ resembles to the concept in the sense of the preceding paragraph. This observation leads to a possible construction of the -resemblance degree of a concept ↵, which can be defined as

⇢ (↵) = M in x2T yp ↵ ⇢ (x).
The resemblance between ↵ and is therefore measured by taking among the typical elements of ↵ those that are the least -resemblant.

Following this definition, the maximally -resemblant concepts are the concepts ↵ such that T yp ↵ ✓ T yp . In particular, such will be the case for the smooth subconcepts of . In general, however, ↵ may have maximal -resemblance without being a subconcept of . For instance, although not all Caravage paintings are figure paintings, we can consider that Caravage paintings maximally resemble figure representations, because typical paintings from Caravage are typical figure representations.

Category-based induction

Category-based induction is the process through which, from a given category, one infers information relative to another category, this inference being based on a link between the source and the target category. In particular, one may ask which attributes of a category remain true for a subcategory or, inversely, which attributes of a subcategory may be raised to the whole category. One may also be interested in resemblance between categories, and look for the attributes that transpose from one category to a resemblant one. These problems can be treated with the tools developed in the preceding sections.

Within-category induction

While the essential attributes of a concept apply to the exemplars of any of its subconcepts, this is no more true for its typical attributes. Typical birds fly, but typical ostriches don't. However, typical birds have feathers with remiges, and such is the case for ostriches. This poses the problem of determining which attributes of a concept remain valid for some subconcept. Knowing for instance that ducks have webbed feet, can we deduce that quacking ducks have webbed feet [START_REF] Connolly | Why stereotypes don't even make good defaults[END_REF]? The inheritance problem is of particular interest in the case of subconcepts obtained through concept determination. To quote [START_REF] Jönsson | The modifier e↵ect in withincategory induction: Default inheritance in complex noun phrases[END_REF] 'Given that an attribute is not universally true of a concept (...), how should one determine whether the predicate should also be considered generically true of the complex concept formed when an adjectival or nominal modifier is applied to the noun'. As will be seen, the answer depends on the smoothness of the target subconcept (recall that a subconcept of ↵ is said to be smooth in ↵ if T yp ✓ T yp ↵).

Smooth subconcepts and non-exceptional modifiers

A determiner will be said to be non-exceptional for ↵ if Ext \ T yp ↵ 6 = ;, that is if there exists at least an exemplar of that is a typical instance of ↵. To-be-red for instance is non-exceptional for the concept to-be-an-apple, while to-be-blue would be an exceptional determiner (in fact, a modifier). This notion of non-exceptional determiner may be seen as a formal definition of the compatible modifiers introduced by [START_REF] Smith | Combining prototypes: a selective modification model[END_REF]. It is tightly linked with that of smoothness: indeed, it can be shown [START_REF] Freund | On the notion of concept I[END_REF] that ? ↵ is a smooth subconcept of ↵ if and only if is non exceptional for ↵. Conversely, it is not di cult to prove that, up to similarity, the concepts obtained from the determination of ↵ by a non exceptional attribute generate all the smooth subconcepts of ↵.

If is a non-exceptional modifier of ↵, ? ↵ is smooth in ↵, and we have therefore T yp ( ? ↵) ✓ T yp ↵, showing that every typical attribute of ↵ applies to the typical instances of ? ↵. For instance, knowing that there exist typical birds that are white and that birds generally sing, we can conclude that white birds generally sing.

This provides a first answer to the within-category induction problem: if is non-exceptional for ↵, inheritance in ? ↵ is total. Note as a particular case, that the above result holds if is itself a typical attribute of ↵: flying-birds will inherit all the typical properties of birds.

Comparison with experimental results: the modifier e↵ect

It has been observed that whatever type of modifier is used, likelihood for an attribute tends to be reduced after modification of a principal concept [START_REF] Jönsson | The modifier e↵ect in withincategory induction: Default inheritance in complex noun phrases[END_REF]). Thus, the authors wrote that 'Sentences were assigned systematically decreasing likelihood ratings as the head noun was modified by a single typical modifier (eg., flightless penguins), by a single atypical modifier (solitary penguins, or by two atypical modifiers (solitary migrant penguins)'.

As far as non-exceptional modifiers are concerned, this definitely contradicts the property evoked above, and therefore questions the proposed model. However, the experiments did not concern simple truth of statements, like 'do quacking ducks have webbed feet': using numbers from 1 to 10, the participants had to indicate the likely truth of a sentence (Ducks have webbed feet, quacking ducks have webbed feet...). It would be interesting to see what answers of the type Y/N would have been given successively to sentences first unmodified, then typically modified, then atypically modified. At any rate, the disparity of some answers with the above result would show that a weak but maybe significant percentage of the participants do not follow this type of model in their categorization process.

The case of exceptional modifiers

When is exceptional for ↵, ? ↵ is no longer smooth in ↵ and the full inheritance property does not apply anymore. Non-flying birds do not inherit the bird typical property of flying. The problem is to determine which attributes of ↵ are preserved in ? ↵. For this it is useful to determine what makes exceptional for ↵.

Suppose that ↵ is a featured concept for which is exceptional. Since

T yp ↵ = Ext ↵ \ ( T (Ext k) k2⌅(↵) ), the set Ext \ Ext ↵ \ ( T (Ext k) k2⌅(↵) ) is empty.
The simplest case where this situation occurs happens when, for a single

↵-characteristic feature k 0 , one has Ext \Ext ↵\Ext k 0 = ;, while Ext \ Ext ↵\( T (Ext k) k2⌅(↵) {k 0 } ) 6 = ;
. No element of T yp ( ?↵) (fully) falls under k 0 . Suppose more precisely that the k 0 -applicability degree of each element of T yp ( ? ↵) is equal to 0. Then one observes that any characteristic feature of ↵ di↵erent from k 0 remains a typical attribute of ? ↵. Indeed, let h be such a feature and suppose by reductio ad absurdum that there exists an element z of T yp ( ? ↵) that does not fall under h. Choose an arbitrary element y of Ext \ Ext ↵ \ ( T (Ext k) k2⌅(↵) {k 0 } ). Then z h y and z k y for any characteristic feature k of ↵, k 6 = k 0 . From this follows that z ⌧ ↵ y. But this contradicts the fact that z is a ⌧ ?↵ -maximal element of Ext ( ? ↵). This shows that h applies to T yp ( ? ↵), and h is therefore a typical attribute of ? ↵.

By this result, we see that inheritance to an exceptional subcategory still holds for the characteristic features that do not directly contradict the determiner. If ↵ is the concept to-be-a-bird, with characteristic feature set ⌅(↵) = {to-fly, to-build-nests, to sing to-eat-seeds}, we can conclude that, typically, walking birds sing, walking birds build nests and walking birds eat seeds.

Over-category induction

Over-category induction is the process through which a property that is known to hold for a subcategory can be raised to a whole category. For instance [START_REF] Connolly | Why stereotypes don't even make good defaults[END_REF], knowing that setters are susceptible to dysplasia, can one conclude that all dogs are susceptible to dysplasia ? This problem may be seen as the converse of that of within-category induction. However, it slightly di↵ers in that one has to distinguish between essential and characteristic attributes. The essential attributes pose no problem in within-category induction, because any essential attribute of a concept remains an essential attribute of its subconcepts (recall (see 3.2) that the essential attributes of a concept are those that apply to every exemplar of the concept). On the contrary, an essential attribute of a subcategory need not hold for the whole category : ducks have webbed feet, but this is not generally true for birds. The problem of over-category induction is therefore the following one: what are the essential attributes of a subcategory that generically apply to the whole category ?

The case of compound concepts

Over-category induction has an evident solution when the considered subconcept is obtained by determining the basic one through one of its typical attributes. In this case indeed if is a typical attribute of ↵, every essential attribute of ?↵ becomes a typical attribute of ↵. This comes from the fact that one has T yp ↵ ✓ Ext , hence T yp ↵ ✓ (Ext \ Ext ↵) = Ext ( ? ↵). Any essential attribute of ? ↵ therefore applies to T yp ↵.

From the fact that birds generally fly and that all flying-birds have feathers with remiges, we can thus conclude that birds generally have feathers with remiges.

Typical subconcepts

Let us consider again the concept to-be-a-bird. When an agent says that the robin is a typical exemplar of this concept, she rests her assertion on the fact that robins inherit all the attributes that a typical bird should have: to fly, to sing, to live in the trees, etc. This inheritance property then extends from individual items to the whole category of robins, thus becoming an essential property of the concept 'to-be-a-robin'. Each exemplar of to-be-a-robin is a typical instance of to-be-a-bird. This leads to the following notion: a concept is a typical subconcept of ↵ if each exemplar of is a typical instance of ↵, that is if Ext ✓ T yp ↵. Note that such a concept is necessarily smooth in ↵.

Let now and be two typical subconcepts of ↵, and h an essential feature of . Suppose that over-category induction holds for h, so that h becomes a typical attribute of ↵. Then, since Ext ✓ T yp ↵, h must be also an essential feature of . This shows that a feature of can extend to a typical attribute of ↵ only if it is an essential feature of all typical subconcepts of ↵. In other words, this feature must not be specific to .

The distinction between specific and non-specific features intervened during the experiments conducted on category-based induction [START_REF] Connolly | Why stereotypes don't even make good defaults[END_REF]. The predicates that were the best candidates for induction to the mother category were the so-called blank predicates. For the participants, these predicates did not bear any special meaning, they were liable to apply to any category that was considered close enough to the tested one. On the contrary, features that were tightly related or specific to the source category had to be discarded.

To make this notion precise, let us say that an essential attribute is nonspecific for a typical subconcept of ↵ if it is shared by all the typical subconcepts of ↵. For instance, to-have-webbed-feet is a non specific feature of ducks as a subcategory of aquatic-birds.

This distinction provides an answer to the over-category induction problem, at least in the case where ↵ is a featured concept. Indeed, let be a typical subconcept of ↵ and k an essential feature of . If k remains a typical attribute for ↵, we have seen that k is non-specific. Conversely, suppose that k is a non-specific feature of . Denote by f 1 , f 2 , . . . f n the characteristic feature features of ↵, and let be the 'pseudo-concept' = f 1 ? f 2 ? . . . ? f n ? ↵. We may see as the concept to-be-a-typical-↵ that parallels the notion of typical object introduced by Desclés [START_REF] Desclés | Logic of determination of objects: How to articulate 'extension' with 'intension' and 'objects' with 'concepts[END_REF]. Note that Ext = Ext ↵ \ T yp ↵, that is Ext = T yp ↵, showing that is a typical subconcept of ↵. This implies now that k becomes an essential feature of , and therefore applies to Ext , hence to T yp ↵. This shows that h is a typical attribute of ↵.

The above result shows that an essential feature of extends to a typical attribute of ↵ if and only if it is non-specific to . For instance, to-have-webbed feet applies to the category of aquatic birds, but not to the whole category of birds.

Induction through resemblance

When a concept ↵ is su ciently close to a concept , one expects that some attributes that hold for the typical instances of will also hold for the typical attributes of ↵: for example some attributional properties should transpose from bats to birds, from horses to cows or from camels to dromedaries.

If ↵ is maximally -resemblant, it follows from section 5.1 that one has T yp ↵ ✓ T yp : any typical attribute of therefore typically applies to ↵.

Apart from this trivial case, one may wonder if a similar answer may hold in the case where the -resemblance degree of ↵, although not maximal, is very close to 1.

Recall that the resemblance degree of ↵ is ⇢ (↵) = M in

x2T yp ↵ ⇢ (x), where ⇢ (x) = ⌃ f 2 ⇧( ) s f f (x) ⌃ f 2⇧(↵) s f . Suppose that ⇢ (↵) 1 | ( )|
⌃ f 2⇧( ) s f . Then, given a typical instance x of ↵, one has f (x) 6 = 0 for every characteristic feature of . Indeed, if h (x) = 0 for some element h of ⌅( ), this would imply ⇢ (x) < 1 | ( )| ⌃ f 2⇧( ) s f , because the salience degree of h, as a characteristic feature of , is greater than | ( )|.

In the particular case where the applicability of the characteristic features of are measured by a two-valued degree function, this result means that if ↵ su ciently resembles to , every characteristic feature of becomes a typical attribute of ↵.

This result shows that Induction through resemblance is accounted for by the proposed model, as was the case for within and over-category induction.

Conclusion

Order relations seem to provide an economical as well as a powerful tool for the study of categorization. For the class of featured concepts, they accurately model the way a given agent may understand a concept. They constitute an interesting alternative that explains and foresees classical problems linked with concept combination or category-based induction. It is to be hoped that experimental studies will confirm the adequacy between this model and the reality.

  This length measures the distance that separates x from Ext ↵. It will be referred to as the membership distance of x, and denoted by µ ↵ (x). Let now N ↵ be the length of a maximal µ ↵ -chain in O. The membership degree µ ↵ is defined, for all objects x, by µ ↵ (x) = 1 µ↵(x) N↵ . One has readily µ ↵ (x) = 1 if and only x 2 Ext ↵, and µ ↵ (x) = 0 if and only if x is maximally distant from Ext ↵. Note that µ ↵ (x) < µ ↵ (y) whenever x µ ↵ y. Example 2 In Example 1, the membership order yields µ ↵ (t) = 1 provided that, for the agent, there exists no animal z such that t µ ↵ z µ ↵ s. Similarly µ Concerning the mouse, the agent may consider that the chain m µ ↵ k µ ↵ b µ ↵ d µ ↵ s is a maximal one, where k stands for a monkey, so that µ

↵ (d) = 1 and µ ↵ (b) = 2. ↵ (m) = 4.

The maximal length of a chain is 4, and the membership degrees are µ ↵

Acknowledgement

Thanks are due to Daniel Lehmann and James A. Hampton for their remarks and suggestions after reading a preliminary version of this paper.


François Thiré

Exporting an Arithmetic Library from Dedukti to HOL *

Keywords: Dedukti, OpenTheory, HOL, Coq, Interoperability Digital Object Identifier 10.4230/LIPIcs

.

Introduction

There are nowadays, many proof systems, e.g. Matita, Coq, HOL Light, etc. but although they share the same goal, these systems are based on different logics. In these systems, Fermat's little theorem requires to prove about 300 hundreds lemmas that are part of the arithmetic library of the system. Elaborate such a library can be a tiresome work and we would like to be able to translate proofs from one system to another.

The aim of this paper is to investigate the possibility to export an arithmetic library from one proof system to others. To achieve this goal, we use the logical framework Dedukti that is able to express several logics. In particular, we will explain how the logic STT∀ βδ , an extension of STT defined in this paper is convenient to express arithmetic statements and can be easily encoded in Dedukti to be afterwords exported to other proof systems. In particular, we will show how we have exported an arithmetic library from STT∀ βδ to the proof systems OpenTheory.

Why interoperability is a problem

The lack of standard in the field makes interoperability between proof systems difficult. There are several problems that may arise at different levels. The first level is on the logical point of view where a statement can have several equivalent definitions. As an example, the well-foudness property for an order can be defined either as:

2.

There is not infinite decreasing sequence For example, the proof system HOL Light implements the first definition while the Coq system implements the second. Moreover, the equivalence between these definitions depends on the logic. Showing the equivalence needs one formulation of the axiom of choice that is not provable in Coq for example. The second level is that two statements can be syntactically different but convertible such as:

1. ∀n, m ∈ N, n + m = m + n 2. commutative +
where commutative is defined as λf . ∀n m, f n m = f m n. Finally at the third level, there is an issue with the name of the statements themselves. For example, the commutativity of addition is called add_comm in Coq v8.6 or plus_comm in HOL4.

But developing from scratch a whole library is difficult and time-consuming. For example proving the Feit-Thompson theorem [START_REF] Gonthier | Engineering mathematics: the odd order theorem proof[END_REF] took several man-years and it is not imaginable to prove such theorems from scratch in several proof systems. It is therefore necessary to develop solutions to make interoperability between proof systems easier.

Logical Frameworks and Interoperability

One one hand, interoperability is not possible in general, since some logics are more expressive than others. For example, one may quantify over proofs in Coq that it is not possible in HOL. On the other hand, it is not conceivable to develop for every pair of proof systems, a specific translation between them because there would be a quadratic number of translations.

Logical frameworks is a solution to overcome these two issues. They are a special kind of formal provers where different logics and proof systems can be specified. Logical frameworks can be used in two different ways to solve this problem that are exposed in Fig. 1 and explained below. Suppose that in the proof system A a theorem thm a needs a proof of theorem thm b proved in the proof system B. In the following, if the system U is a logical framework and A is a proof system, we denote U [A] the encoding of A in U .

A first solution is to use the logical framework to encode both proofs and combined them. Then check that the combined proof (understandable by the logical framework) is correct. This solution raises several problems: there are two definitions for the same objects, and one needs to prove that both representations are isomorphic; a second problem is that the proof is also expressed in a logic that is not obviously consistent even if it is the union of two consistent logics. This solution has already been explored by Cauderlier in [START_REF] Cauderlier | Focalize and dedukti to the rescue for proof interoperability[END_REF].

In this paper, we are interested in a second solution. This solution as described in second picture of figure 1 can be decomposed in three steps. We first translate thm A from the proof system A to its encoding in U [A]. Then translate thm a from U [A] to U [B]. And finally translate thm a from U [B] to the proof system B. In this process, the first and last steps are total functions. However, the second step is a partial function since the translation is not always possible. For example, proof irrelevance is not expressable in HOL but it is in CiC. Also, one might think that translating proofs from U [A] to U [B] is quite similar to translating proofs from A to B, and therefore this step is also specific for the two proof systems A and B. This is not completely true for the following reasons:

Working inside a logical framework may unify the transformations: Inductive types from Matita or Coq will be encoded the same way in a logical framework. Moreover, if one wishes to transform inductive types in the theory encoded in that logical framework, that transformation does not depend on the prover where the terms are coming from but only on the encoding. It is possible to cut the translation in smaller steps that can be shared between several transformations. If a system A is a subsystem of a system B, then one can directly translate proofs from the encoding of A to the system B directly.

Contribution

For this work, we are going to use Dedukti as our logical framework. Dedukti is based upon the λΠ-calculus modulo theory, an extension of LF [START_REF] Harper | A framework for defining logics[END_REF] with rewrite rules [START_REF] Cousineau | Embedding pure type systems in the lambda-pi-calculus modulo[END_REF]. This extension has three main advantages: It is easier to express different systems in Dedukti than in LF Proofs encoded in Dedukti are smaller thanks to rewrite rules. Encodings can be shallow (defined in section 2) in most cases (such as STT∀ βδ )

The last property mentioned above is important since one problem that could arise with translations and encodings is to pollute statements so that statements become unreadable and unusable. This can be avoided thanks to shallow encodings.

Our aim is to fully export the Fermat's little theorem coming from an arithmetic library encoded in STT∀ βδ to OpenTheory and Coq. OpenTheory is already an interoperability tool that allows to share proofs between several implementations of HOL. Therefore, targeting OpenTheory allows us to get the proofs in every system that support OpenTheory. We have decided to take an arithmetic library for two reasons. First, because arithmetic is a branch of mathematics that is very common and therefore we can expect that every formal provers is capable of proving arithmetic statements. Second, this library is neither too small nor too big to make experimentations (340 lemmas).

STT∀ βδ is an extension of STT with prenex polymorphism and is modulo βδ 1 . We think that this logic is particularly well suited to export arithmetic proofs to other proof systems.

2

Dedukti and STT∀ βδ

Dedukti

Dedukti is a logical framework that implements the λΠ-calculus modulo theory, a calculus that extends LF with user-defined rewrite rules. These rules might are used in the convertibility test. The syntax and the type system of λΠ-calculus modulo theory are presented in

Terms A,B,t,u ::= Kind | Type | Πx : A. K | A B | λx A . B | x Contexts Γ ::= ∅ | Γ, x : A | Γ, t → u Figure 2 Dedukti syntax [ ] well-formed empty ctx Γ A : s Γ t : A A ≡ βΓ B Γ t : B conv Fig. 3 λΠ typing system
Fig 2 and 3. The type system is not complete because we do not present how to derive the judgment Γ t → u. A complete description of the system can be found in [START_REF] Saillard | Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique)[END_REF]. Roughly, a rewrite rule t → u is well typed when the types of t and u are the same. One advantage of using rewrite rules is that more systems can be encoded in Dedukti using a shallow encoding. Such encoding has the two following properties: A binder of the source language is translated as a binder in the second language (using HOAS for example) and the typing judgment from the source language is translated as a typing judgment for Dedukti. This means that we can use the type checker of Dedukti to check directly if a term encoded in Dedukti is well-typed.

The next two paragraphs are dedicated to the STT∀ βδ system and its (shallow) encoding in Dedukti.

STT∀ βδ

Before going down to a full description of STT∀ βδ , we want to stress one our two points about interoperability. This will explain some choices made in STT∀ βδ such has it is possible to declare constants.

How interoperability should work

Let's say that in the system A, I have a proof of ∀ (x y : N), x + y = y + x, in general the system do not define natively the type N nor the operator +, these types and operators are user-defined. In Coq, N is a inductive type, but in HOL, it is a type operator. The same occurs for + where in Coq it is define has a fixed point but in HOL it is defined using two

François Thiré Access XX:5

equalities (there is no fixed point operator). Let denotes + A the operator + in the system A.

A naive inspection on interoperability could be seen as how to translate the theorem

Σ A ; ∅ ∀ (x y : N A ), x A + y = y + A x to Σ B , ∅ ∀ (x y : N B ), x B + y = y + B x
. But this is problematic for the following reasons: Definition of a type is not unique. For example, in Coq, natural numbers have three different definitions. Which one should be used? If one use an intermediate system to translate these proofs, the encoding from the first system to the intermediate may degrade the original definition. Reconstitute the original type or constant might be difficult. For example, the inductive of the natural numbers is translated as four declarations (N, 0, S, the recursor definition) and two rewrite rules in Dedukti. But from these declarations and these rewrite rules, it is difficult to identify that this correspond to inductive definition of natural numbers because we cannot rely on the names. Finally, if one wants to automatize this translation, it is in general impossible to guess the definition of every types and constants involved in the development inside the target system. For example, if one identify in the previous example that this is the natural numbers, how to automatize the translation to the target system without hard-coding the definitions of some pre-define types and pre-define constants?

For all of these reasons, our translation process produces a library where the definition of some constants are axiomatized.

The target user can use the definition he wants as long as the axioms related to the constant are provable The intermediate do not care of the meaning of some declarations nor some axioms.

It translates simply what it sees.

There is no more problems regarding automation since there is no guess nor hard-coding to do

A description of STT∀ βδ

STT∀ βδ is an extension of STT with prenex polymorphism and type operators. A type operator is constructed using a name and an arity. This allows to declare types such as bool, nat or α list. The polymorphism of STT∀ βδ is restricted to prenex polymorphism as full polymorphism would make this logic inconsistent 2 [START_REF] Coquand | An analysis of girard's paradox[END_REF]. The STT∀ βδ syntax is presented in Fig. 4. Introducing types operator makes Prop and → redondante since they can be declared as type operators, respectively of arity 0 and 2. But these two types have a particular role in the typing judgment that is why we let them in the syntax. Also, STT∀ βδ allows to declare and define constants. Declaring constants is better for interoperability as discussed in section 2.2.1. The typing system and the proof system are as expected and presented in Fig. 5 and Fig. 6. Also notice that we identify in STT∀ βδ the terms t and t if they are convertible modulo β and δ (unfolding of constants).

The meta theory of STT∀ βδ is proved in the full version of this paper.

Example: Equality in STT∀ βδ

This paragraph explains how to implement Leibniz equality (denote = L ) in STT∀ βδ . Its type will be ∀X . X → X → Prop and can be inplemented as: λX . λx X . λy X . ∀P P →Prop . P x ⇒ P y. From this definition, it is possible to prove that = L is reflexive expressed by the following statement A X. ∀x X . x = L x using the following derivation tree:

= L ; X, x : X; P x P x assume = L ; X, x : X; ∅ P x → P x ⇒I = L ; X, x : X; ∅ x = L x conv = L ; X; ∅ ∀x X . x = L x ∀I = L ; ∅; ∅ A X. ∀x X . x = L x A I

Dedukti[STT∀ βδ ]

Thanks to Higher-order Abstract syntax (HOAS), we have a shallow encoding of STT∀ βδ in Dedukti shown in 7.

For the types, we declare two constants type and ptype that are respectively the types for the types schema and the type of STT∀ βδ . Therefore every type of STT∀ βδ will be encoded François Thiré Access XX:7 Exporting an Arithmetic Library from Dedukti to HOL For the terms, since the encoding is shallow, we do not need constants for abstractions and applications. We only need two constants for ∀ and ⇒ that encode respectively f orall and impl. We also need another constant to encode polymorphic propositions with f orallK bool . Finally, we add rewrite rules to make the encoding works. For example we want that an encoding of a term of type Prop → Prop of STT∀ βδ is a abstraction in Dedukti. This is possible thanks to the rewrite rule:

X ∈ Γ Σ; Γ X wf WF var Σ; Γ Prop wf WF prop Σ; Γ A wf Σ; Γ B wf Σ; Γ A → B wf WF fun Σ Γ wf Σ Γ, X wf WF ctx var (p : n) ∈ Σ Σ; Γ A i wf Σ; Γ p A 1 . . . A n wf WF tyop app ∅ wf WF empty Σ Γ wf Σ; Γ A wf Σ Γ, x : A wf WF ctx var Σ wf p ∈ Dom(Σ) Σ, (p : n) wf WF tyop Σ wf cst ∈ Dom(Σ) F V (T ) = ∅ Σ, cst : T wf WF cst decl Σ wf cst ∈ Dom(Σ) Σ; ∅; ∅ τ : T Σ, cst = τ : T wf WF cst defn Σ wf Σ Γ wf C, x : A x : A var C f : A → B C t : A C f t : B app C, x : A t : B C λx A . t : A → B abs C t : Prop C u : Prop C t ⇒ u : Prop imp C, x : A t : Prop C ∀x A . t : Prop forall C, X t : T C λX . t : A X. T poly intro F V (B) ⊆ C C c : A X. T C c B : T [X := B] cst app typeof (C, cst) = T C cst : T cst C, X τ : Prop C A X. τ : Prop Poly prop
C t : Prop C, t t assume C t C t ⇒ u C u ⇒E C, t u C t ⇒ u ⇒I C ∀x A . t C u : A C t[x := u] ∀E C, x : A t x ∈ C C ∀x A . t ∀I C A X. τ F V (A) ⊆ Γ C τ [X := A] A E C, X τ C A X. τ A I C t t

etap (p (arr l r)) --> eta l -> eta r

A STT∀ βδ constant will be encoded by a Dedukti constant. We explain below how to translate Leibniz equality and a reflexivity proof in Dedukti[STT∀ βδ ]. The full translation can be found in the full version of this paper.

A proof of reflexivity:

The translation of Leibniz equality in Dedukti[STT∀ βδ ] is as follow. First the type of = L is translated as: etap (forallKtype (X:type => arr X (arr X bool))) then its definition is translated as A:type => x:(eta A) => y:(eta A) => forall (arrow A prop) (P:(eta (arrow A prop)) => impl (P x) (P y)).

Finally, the proof of refl is translated as that is of type

f ) → x type → etap (f x) eps(f orall t f ) → x eta t → eps (f x) eps(impl l r) → eps l → eps r eps(f orallK bool f ) → x type → eps (f x)
eps (forallKbool (X:type => forall X (x:(eta X) => leibniz X x x))
which is the translation of

A X. ∀x X . x = s x
Notice that each introduction rule leads to the introduction of an abstraction while an elimination rule leads to the introduction of an application.

One can prove that this encoding is sound and complete: every statement thm are provable in STT∀ βδ if and only if the thm is provable in Dedukti[STT∀ βδ ].

Theorem 3 (Soundness and completness). This encoding is sound and complete

Proof. By mutual induction on the derivability of each judgment.

OpenTheory

HOL (for higher order logic) is a logic that is implemented in several systems with some minor differences. OpenTheory is a tool that allows to share proofs between several implementations of HOL. Since we are targetting OpenTheory, we will mostly refer to the logic defined by OpenTheory. It is a logic inspired by Q 0 where the only logical connective is the equality. Terms are the one of STLC with an equality symbol while the type system extends the one of STLC by declaring type operators and prenex polymorphism. The proof system of OpenTheory can be found in Fig. 8.

XX:10 Exporting an Arithmetic Library from Dedukti to HOL

t t assume Γ t = u Γ λv.t = λv.u absThm Γ t 1 = u 1 ∆ t 2 = u 2 Γ ∪ ∆ t 1 t 2 = u 1 u 2 appThm t 1 , . . . , t n u axiom (λx.t)u = t[u/x] β Γ t ∆ u (Γ -u) ∪ (∆ -t) t = u deductAntiSym Γ t ∆ t = u Γ ∪ ∆ u eqMp Γ t ∆ u (Γ -u) ∪ ∆ t proveHyp t = t refl Γ t Γσ tσ subst Γ t = u Γ u = t sym Γ t 1 = t 2 ∆ t 2 = t 3 Γ ∪ ∆ t 1 = t 3
trans Fig. 8 OpenTheory proof system

STT∀ βδ vs OpenTheory

One may notice that the two systems STT∀ βδ and OpenTheory are quite close. However, there are some differences that makes the translation from STT∀ βδ and OpenTheory tedious:

Terms in OpenTheory are only convertible up to α conversion while in STT∀ βδ it is up to α, β, δ conversion All the connectives of OpenTheory are defined upon the equality symbol, while in STT∀ βδ they are defined upon ∀ and ⇒ connectives Prenex polymorphism in OpenTheory is implicit. All free variables in a type are implicitly quantified while in STT∀ βδ it is explicit These differences lead to three different proof transformations: 1. Encode the ∀ and ⇒ connectives using the equality of OpenTheory 2. Explicit each application of the conversion rule 3. Finally, we get rid of the type quantifier

Encoding ∀ and ⇒ using the equality

A first idea to encode STT∀ βδ logic in OpenTheory would be to axiomitize all the rules of STT∀ βδ and then translate the proofs using these axioms. But translating a rule to an axiom in OpenTheory requires to use the implication. But since OpenTheory does not know what is an implication, suche axioms would be unusable since it would not be possible to use the modus ponens to eliminate the implication itself. Therefore, one must find an encoding of the ∀ and ⇒ connectives such that the rules of STT∀ βδ ara admissible. Such encoding is already known from Q 0 [START_REF] Andrews | An introduction to mathematical logic and type theory -to truth through proof[END_REF]. This encoding preseneted in Fig. 9 uses two other connectives:

and ∧ that can be defined in OpenTheory. Note that in this encoding, the definition of may remain abstract but the definition of ∧ is needed to prove the admissibility of the rules of STT∀ βδ . These definitions can be easely translated as axiom in OpenTheory.

François Thiré Access

XX:11

x ∧ y :≡ λf . f x y = λf . f

x → y :≡ x ∧ y = x ∀x.P :≡ λx. P = λx. We stress here that it is really important to axiomatize these definitions and not to define new constants. The difference is that it will be possible to instantiate latter these connectives by the true connectives of HOL as long as these axioms can be proved regardless of their definition in HOL. Also, these axioms are not too strong to satisfy because in HOL, propositional extensionality 3 is admissible. Using this encoding, it is possible to derive all the rules of STT∀ βδ in OpenTheory using the four axioms below. Below, we proof the admissibility of the ∀ I rule:

Suppress the type quantifier

Since OpenTheory implicitely quantifies over free types variables, we need to remove the ∀ constructor on types and the A connective. But we cannot just remove these symbols, we also need to avoid capture. To do that, we need to do two things:

Ensure that in each type, all the bound variables have a different name Replace each occurence of the A E by a renaming step with the subst rule of OpenTheory So

C A X. τ F V (A) ⊆ Γ C τ [X := A] A E is translated as C τ Z f resh C τ [X := Z] C τ [Z := A]

From Dedukti[STT∀ βδ ] to Coq

Going from STT∀ βδ to Coq is really easy since all the constructions in STT∀ βδ are possible in Coq. However, some subtleties comes from types operators and constant declarations. A type operator such as nat and the two declared constants 0:nat and S : nat -> nat would be ideally translated as an inductive type. However, it is really difficult (maybe impossible?) to do that for all inductive types in an automatic way. But this is not a real problem since it is possible to declare axioms and parameters in Coq. A more general observation is made in 2.2.1. Moreover, using the Curry-De Bruijn correspondance, it is possible to translate every proof STT∀ βδ into a Coq terms. In our case, since we start from Dedukti[STT∀ βδ ], we already have the lambda term. Getting back to our reflexivity proof. One can translate the equality = s as the following definition in Coq Definition = : forall X:Type, X -> X -> Prop := fun X:Type => fun x:X => fun y:X => forall (P:X -> Prop), P x -> P y.

Then the proof of reflexivity can be translated from the Dedukti[STT∀ βδ ] as the coq definition Definition refl = : forall X:Type, forall x:X x = x := fun X:Type => fun x:X => fun h:P x => h.

One may notice that going from Dedukti[STT∀ βδ ] consists mostly to remove etap annotations.

5

The arithmetic library

We have implemented these transformations and we have used them on an arithmetic library encoded in Dedukti[STT∀ βδ ]. The results can be found in the table 1. These results show that the difficult translation needed for OpenTheory impacts on the type checking time and the size of the library. this time seems reasonable. The final statement for Fermat's litthe theorem we get in Coq is the following: Definition congruent_exp_pred_SO : forall p a : nat, prime p -> Not (divides p a) -> congruent (exp a (pred p)) (S O) p.

In the library, the constants prime, congruent and pred are defined by the library while the constants exp, Not, O and S are declared by the library and should be instantiated by the user. Once these constants are instantiated (with a functor mechanism of Coq for example), the theorem is ready to use. The instantiation for these constants cannot be anythyng, they have to satisfy some axioms. For the constant exp, the two following axioms has to be satisfied: For the arithmetic library, one has to give 40 definitions for constants and prove 80 axioms. All the constants definitions follow from their name or from the axioms they have to satisfy, and hence the axioms are easy to prove.

Conclusion

In this paper, we used Dedukti to export an arithmetic library from the STT∀ βδ logic to the proof system Coq and the proof system OpenTheory. We showed how STT∀ βδ is a simple logic that can be encoded easely in Dedukti and is powerful enough to express arithmetic proofs. The differences between OpenTheory and STT∀ βδ makes the translation from the later to the former a bit tedious. To overcome this issue, we have isolated three main

François Thiré Access XX:15 differences between the two systems and for each difference, proposed a translation. While the translation to OpenTheory is tedious, we show how the translation to Coq is very easy since it is basically just an embedding. Finally, we propose a framework for interoperability between systems so that it is effectively possible to reuse a developement from one system to another.

Future work

We would like to export this library to other proof systems such as PVS or Agda. While for Agda, the translation should be similar to the one of Coq, for PVS this is a challenge since there no proof term but only tactics. In other word, each rule should be translated by an application of one or more tactics and the behaviour can make this translation a bit tricky. We also would like to export more arithmetic proofs and other proofs that could be encoded in the logical framework Dedukti. Though this work requires to be able to translate these proofs in Dedukti [STT].

Finally, we hope that this work is the beginning of a process that could lead to a standardization of proofs. A first step would be to standardize this arithmetic library so that every proof systems share the same arithmetic library.

Figure 1

 1 Figure 1 Interoperability with a logical framework

Fig. 5

 5 Fig. 5 STT∀ βδ typing system

Figure 7

 7 Figure 7 Signature for STT∀ βδ in Dedukti

Figure 9

 9 Figure 9 Encoding of ∀ and → in Q0

  Axiom sym_eq_exp_body_0 : forall n : nat, (S O) = (exp n O). Axiom sym_eq_exp_body_S : forall n m : nat, (times (exp n m) n) = (exp n (S m)). It is quite easy to come with the following definition for exp: Fixpoint exp (n m : nat) : Datatypes.nat := match m with | O => S O | S m => n * exp n m end

Table 1

 1 Arithmetic library translation

		Dedukti[STT] OpenTheory Coq
	size (mb)	1.5	41	1
	translation time (s)	-	18	3
	time to check (s)	0.1	13	6

δ meaning the (un-)folding of constants

Γ A : s Γ, x : A well-formed ctx sort Γ t → well-formed Γ, t → u well-formed ctx → Γ well-formed Γ Type : Kind ctx Type Kind Γ well-formed (x : A) ∈ Γ Γ x : A variable Γ A : Type Γ, x : A B : s Γ Πx A . B : s prod Γ A : s Γ, x : A B : s Γ,x : A t : B Γ λx A . t : Πx A . B abs Γ t : Πx A . B Γ t : A Γ t t : B app

Π C, x : A t x ∈ C C ∀x A . t Below, Γ is the translation of C in OpenTheory 4 . Π Γ t Γ Γ t = Γ λx. t = λx. Γ ∀x. t x = (λx. t = λx. ) Γ (λx. t = λx. ) = ∀x. t x Γ ∀x. t xThe right branch is closed thanks to the forall axiom. After this translation, the syntax of the terms is the same as STT∀ βδ except that we add an equality symbol and the connectives ∀ and ⇒ become defined constants.3.1.2 Eliminate β, δ reductionsThe decidability of STT∀ βδ relies on the fact that the term rewriting system defined by → β and → δ is convergent. This means that to decide is t ≡ βδ u we can compute the normal form of t and u and check that they are equal up to α. This means that the conversion testΓ t Γ t ≡ βδ u Γ u can be reduced to 3 ∀P, Q, (∀x, P x = Q x ⇒ P = Q)[START_REF] Cauderlier | Focalize and dedukti to the rescue for proof interoperability[END_REF] In OpenTheory, free variables such as x does need to appear inside the context

Γ C[t] → βδ C[u]This is done inductively on the structure of C. To do that, we need an equality judgment that goes through the context. In OpenTheory, there are two rules to handle abstractions and applications. We need to derive such rules for the connectives of STT∀ βδ . Here we show only the admissibility ofΓ p = p Γ q = q Γ p ⇒ q = p ⇒ q Γ, p ⇒ q p ⇒ q Γ, p p Γ p = p Γ p = p Γ, p p Γ, p ⇒ q, p q Γ q = q Γ, p ⇒ q, p q Γ, p ⇒ q p ⇒ q . . . Γ p ⇒ q = p ⇒ qWe put dots for the right part of the DeductAntiSym rule because the proof is symmetric.From this rule, it is easy to derive the rule for context:Γ C[t] = C[t ] Γ u = u Γ C[t] ⇒ u = C[t ] ⇒ u

Since equality in OpenTheory is also modulo α, the last judgment is not a problem anymore. The problem remains to translate t → βδ u in OpenTheory.

To handle β and δ OpenTheory has two rules:

However we need to apply these rules inside a context. In STT∀ βδ , a context can be described by the following grammar:

The goal is to derive the following rule for every context C: