Je n'ai pas (encore ?) lu "Le fantôme de la transparence", mais je pense que tu sautes un peu du coq (sic) à l'âne.
Oui, je saute du coq à l'âne, cette question m'est juste venue à l'esprit par association d'idée, je ne sous-entendais pas un lien fort entre les deux concepts de tests.
dans les derniers machins de Girard [...]
Il y a une chose qui m'intringue chez Girard dans sa lecture de la syllogistique aristotélicienne. Il met systématiquement en rapport la forme Barbara (les animaux sont mortels, or les hommes sont des animaux, donc les hommes sont mortels) avec la transitivité de l'implication (composition des morphismes catégoriques pour la logique classique, composition des opérateurs hilbertiens pour la logique linéaire) :
(*|- A -> B |- B -> C----------------------- |- A -> C*)fungfx->f(gx);;-:('a->'b)->('b->'c)->'a->'c=<fun>
là où, pour moi, il m'apparait plus évident que Barbara c'est du sous-typage structurel :
S <: M M <: P
------------------
S <: P
Barbara : c'est la transitivité du sous-typage, raison pour laquelle les prédicats sont unaires chez Aristote et qu'il n'y a aucune distinction logique entre sujet et prédicat : quelque chose qui ne peut être pensée que comme sujet mais jamais comme prédicat est une substance, concept qui appartient à la métaphysique mais non à la logique (comme un terme qui ne peut être également vu comme un type).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Questions en vrac.
Posté par kantien . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2. Dernière modification le 18 octobre 2017 à 15:08.
Oui, je saute du coq à l'âne, cette question m'est juste venue à l'esprit par association d'idée, je ne sous-entendais pas un lien fort entre les deux concepts de tests.
Il y a une chose qui m'intringue chez Girard dans sa lecture de la syllogistique aristotélicienne. Il met systématiquement en rapport la forme Barbara (les animaux sont mortels, or les hommes sont des animaux, donc les hommes sont mortels) avec la transitivité de l'implication (composition des morphismes catégoriques pour la logique classique, composition des opérateurs hilbertiens pour la logique linéaire) :
là où, pour moi, il m'apparait plus évident que Barbara c'est du sous-typage structurel :
Barbara : c'est la transitivité du sous-typage, raison pour laquelle les prédicats sont unaires chez Aristote et qu'il n'y a aucune distinction logique entre sujet et prédicat : quelque chose qui ne peut être pensée que comme sujet mais jamais comme prédicat est une substance, concept qui appartient à la métaphysique mais non à la logique (comme un terme qui ne peut être également vu comme un type).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.