Re: Reason

Je comprends l'appréhension qu'a pu susciter ma réponse, mais dans un premier temps je n'ai pas vu comment faire plus court. Il me fallait poser les termes du problèmes (d'où l'exposition des notions de genres et d'espèces), expliquer comme lire les règles de déduction à la Gentzen et illustrer par des exemples un cas où une classe héritant d'une autre n'en était pourtant pas un sous-type.

Je vais essayer de condenser le cœur de l'argumentaire (le nervus probandi, comme on dit).

Oublions le Gamma et le code OCaml.

Laissons de côté le Gamma, qui n'est nullement essentiel pour comprendre le problème, et le code d'illustration en OCaml. L'essentiel tient déjà dans ce qui était simple à comprendre :

Je pense (du moins je l'espère) que ce que je viens d'exposer doit être facilement compréhensible.

Oui ;)

Ensuite on va considérer deux classes dans une syntaxe de mon invention (c'est proche de mon exemple final).

classe A = {
 attr1 : T1 ;
 meth : A -> A
}
classe B herite A = {
 attr2 : T2 ;
 meth : B -> B
}

Voilà deux classes A et B, où la deuxième dérive de la première, ajoute un attribut et surcharge leur méthode commune meth. Pour que B soit un sous-type de A, il faudrait que les types de leurs composants communs soient des sous-types les uns des autres. Autrement dit, il faudrait que T1 <: T1 (types de attr1) et que B -> B <: A -> A (types de meth).

Tout type étant un sous-type de lui-même, on a bien T1 <: T1, mais la deuxième condition ne peut être vérifiée. En voici la raison :

• les fonctions qui acceptent des animaux en entrée, acceptent des hommes en entrée
• les fonctions qui retournent des chats, retournent des félins.

Or, sur le plan de la subordination des genres et des espèces, on a : homme <: animal et chat <: félin. Donc en condensant les deux principes précédents et en faisant abstraction des concepts impliqués, on aboutit à la règle de déduction suivante :

T1 <: S1 S2 <: T2 homme <: animal chat <: félin
--------------------- --------------------------------
S1 -> S2 <: T1 -> T2 animal -> chat <: homme -> félin

Ainsi pour pouvoir prouver la condition B -> B <: A -> A, il faudrait satisfaire les deux prémisses de la règle ci-dessus, à savoir : A <: B et B <: A. Ce qui reviendrait à dire que les deux classes sont identiques, ce qui n'est évidemment pas le cas.

Revenons à Gamma et au code OCaml.

Ce n'est vraiment pas un point très important à comprendre, le calcul des séquents est surtout un outil qui sert aux personnes étudiant les preuves (les théoriciens de la démonstration); comme le dit la page wikipédia : « le calcul des séquents doit se penser comme un formalisme pour raisonner sur les preuves formelles plutôt que pour rédiger des preuves formelles ».

La lettre grecque \Gamma dans les notations à la Gentzen sert à désigner l'ensemble des hypothèses utilisées pour prouver la thèse qui se trouve à droite du symbole \vdash. Prenons le problème de géométrie suivant :

Soit ABC un triangle isocèle en A et appelons O le milieu du segment BC. Montrer que la droite (BC) est perpendiculaire à la droite (OA).

Ici le contexte Gamma c'est l'énoncé du problème (auquel il faudra rajouter quelques axiomes de la géométrie euclidienne), et à droite du symbole de thèse on aura le résultat à prouver.

Pour tes questions sur le code OCaml, chimrod t'a en partie répondu. En ce qui concerne le syntaxe let ... in, c'est ainsi que l'on définit des variables locales en OCaml. Exemple dans la boucle interactive :

let i = 1 and j = 2 in i + j;;
- : int = 3
i;;
Error: Unbound value i

Les variables i et j n'existent qu'au sein de l'expression i + j, elles sont locales et n'existent plus une fois cette dernière évaluée. Cela étant la boucle me répond que la somme i + j est de type int et vaut 3. Ce qui en notation de Gentzen revient à dire que le type checker a pu prouver ce séquent :

i : int , j : int , (+) : int -> int -> int |- i + j : int

Vois-tu ce qu'est le contexte Gamma dans cet exemple ?

Pour terminer ma réponse, la règle que tu cites en fin de ton message :

Gamma |- t : S S <: T
-----------------------
 Gamma |- t : T

n'était pas celle utilisée dans mon exemple. Mon exemple avait pour but de répondre à ta question qu'est-ce que Gamma ? (à savoir un contexte, un environnement), et ensuite je réécrivais cette règle pour pouvoir la traduire en français. C'est néanmoins cette règle qui est utilisée dans un bout de code qui se situe un peu plus loin :

let op' = new point2d 1. 2.;;
val op' : point2d = <obj>
move_x 0.1 (op' :> point);;
- : point = <obj>

Dans ce contexte on sait que op' : point2d, de plus on a bien point2d <: point, et donc le type checker peut conclure qu'on a le droit de considérer op' comme étant de type point.

Reste-t-il des points obscurs dans mon exposé ?

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.