Il existe une opération fondamentale qu'est l'application d'une fonction sur un élément. Et comme il existe deux sens d'écriture, il faut toujours avoir à l'esprit qu'il existe deux tels opérateurs, l'un anglais, noté `"·"`, prenant une fonction et un élément, `f"·"x`, et retournant l'image par la fonction de l'élément (ou l'élément indéfini si `x` est hors domaine), l'autre français, noté `"￪"`, en mettant la fonction en exposant de son argument, `x^f`. Déja, l'approche faite par cette première remarque est éminament combinatoire, et elle introduit un élément particulier qu'est l'indéfini, noté `"⧫"`, ce que retourne une fonction appliquée à un élément hors de son domaine de définition.
Mais nous ne voulons pas développer une science purement combinatoire, nous l'associons tout de suite à une structure algébrique qui lui donne un sens intuitif beaucoup plus riche, sans pour autant restreindre le modèle d'une quelconque façon.
Les fonctions sont transformées en applications grâce à la définition de l'élément indéfini, noté `"⧫"`, qui est le résultat d'une fonction appliquée à un élément hors de son domaine de définition, et que l'on rajoute à l'ensemble sur lequel opère la fonction en tant qu'application. Mais on désignera ces applications toujours comme des fonctions, puisqu'on a donné à cet élément `"⧫"` ce sens particulier pour justement pouvoir construire des fonctions. D'ailleurs, cet élément `"⧫"` n'est pas distingué des autres si ce n'est par le seul fait d'avoir été choisi pour nous permettre de construire des fonctions au sens où nous l'entendons.
Une étude précise marquerait là encore un schisme, deux modèles, l'un avec cet élément `"⧫"` définissant la notion de fonction sous forme d'application, et l'autre sans cet élément n'utilisant que des applications qui peuvent d'ailleurs désigner des fonctions en prenant d'autres éléments pour désigner le hors domaines. Somme-toute, la distinction ne porte que sur le choix d'un élément et sur le sens sémantique donner aux applications retournant cet élément. Notez qu'une fonction peut s'appliquer sur l'élément indéfini `"⧫"` pour lui donner une image quelconque. Ce qui est important, c'est que la composition de fonctions interprétés ici comme des applications soit toujours associative.
Dans une approche ensembliste, nous considérons un ensemble d'élements `E`, et l'on considère l'ensemble des fonctions de `E` dans `E` noté `E^E` puisque les fonctions sont définies comme des applications. Puis, comme les fonctions évoquées doivent constituer des éléments de `E` et réciproquement, on souhaite poser une bijection `varphi` de `E` sur `E^E`, ce qui est impossible car la cardinalité de `E^E` est toujours strictement supérieure à celle de `E` (sauf pour les singletons). On pose donc une application injective `varphi` de `E` dans `E^E` où toutes les fonctions ne sont pas atteintes. On plonge ainsi `E` dans `E^E`.
On prend quand même la précaution de choisir un ensemble `E` de cardinalité infinie, et d'atteindre au moins toutes les fonctions de `E` sur `E` qu'il est possible de définir. Comme toute définition de fonction est une formule finie écrite dans un langage d'alphabet fini, nous savons que cela est possible grâce à l'axiome du choix et au théorème affirmant que « la cardinalité de l'ensemble des mots finis d'un alphabet fini est dénombrable », et peut donc être plongé dans un ensemble infini. Ainsi, l'application `varphi` assigne à chaque élément de `E` un second rôle distinct unique, celui d'une fonction de `E` dans `E`. Et réciproquement toutes fonctions de `E` dans `E` qu'il est possible de définir est envoyée par l'application inverse `varphi^-1` sur un élément distinct unique de `E`.
Le modèle peut s'agrandire encore en incorporant dans son langage un ensemble de fonctions quelconque de `E` dans `E` mais dont la cardinalité ne doit pas dépasser celle de `E`, grâce au théorème affirmant que « la cardinalité de l'ensemble des mots finis d'un alphabet infini est de même cardinalité que celle de son alphabet ».
Puis, afin de simplifier les formules nous ne désignerons jamais l'application `varphi`, on laissera à la syntaxe le soin d'enlever l'ambiguité des rôles des éléments, à savoir quel rôle ils jouent si c'est leur premier rôle d'élément ou leur second rôle d'application.
Le modèle combinatoire ainsi construit n'admet pas d'éléments distincts ayant le même second rôle. C'est le choix d'une application `varphi` injective de `E` vers `E^E`, qui se traduit par l'axiome d'égalité d'application :
`AAxAAy, (AAz, x(z)"="y(z)) => x"="y`
On souhaite rester simple et au plus proche de ce que les gens ont l'habitude d'utiliser. C'est pourquoi notre opérateur binaire point `"·"` est choisi avec une syntaxe centrée. Le terme `f"·"x` signifie l'application de la fonction `f` sur l'élément `x`. Cet opérateur n'est pas associatif. Pour éviter l'usage intensif des parenthèses, lorsque plusieurs tels opérateurs se succèdent on fixe une priorité sur l'opérateur de gauche, faisant que par exemple :
`f"·"x"·"y"·"z = ((f"·"x)"·"y)"·"z`
L'autre choix syntaxique consistant en une priorité sur l'opérateur de droite a été écarté car il correspond à l'utilisation de l'opérateur de composition de fonction noté `∘` qui a la propriété d'être associatif, une propriété suffisament importante pour justifier la définition de cet opérateur :
`f"·"(g"·"(h"·"x)) = (f"∘"g"∘"h)"·"z`
Parcontre l'opérateur d'application point `"·"` est de priorité syntaxique plus grande que celle de la composition `"∘"`. Et on pourra constater ce choix dans la quasi-totalité des langages de programmation. Cet opérateur de composition se définie grace à l'axiome d'égalité des applications, en définissant ce que vaut son résultat appliqué à un élément quelconque `x`, comme suit :
`AAfAAgAAx, (f"∘"g)"·"x = f "·"(g"·"x)`
L'application d'une fonction `f` sur un élément `x` se note habituellement en notation anglaise `f(x)`. Et si le résultat est une fonction que l'on souhaite appliquer à `y`, on notera `f(x)(y)` et ainsi de suite. Cette écriture correspond à celle de l'opérateur point `"·"` précédement décrite, où l'on remplace le point `"·"` par une parenthèse ouvrante marquant un appel de fonction et où on ajoute une parenthèse fermante à la fin du second argument. La parenthèse ouvrante possède ainsi deux significations possible, l'appel d'une fonction, et par defaut d'appel elle constitue une simple priorisation syntaxique de son contenue par rapport aux opérations l'exterieur. Ainsi nous avons par exemples :
`f"·"x"·"y"·"z = f(x)(y)(z)`
`f"·"(g"·"(h"·"x)) = (f"∘"g"∘"h)"·"x = f(g(h(x))) = (f"∘"g"∘"h)(x)`
Et la définition de la composition de fonction `"∘"` se note :
`AAfAAgAAx, (f"∘"g)(x) = f(g(x))`
L'opérateurs d'application d'une fonction sur un élément, en notation française et non plus anglaise comme précédemment, se note en mettant la fonction en exposant de son argument, ou explicitement avec le symbole d'opérateur `"￪"`. Et la composition de fonctions, en notation française, se note implicitement par simple juxtaposition des fonctions mais dans l'ordre inverse, ou explicitement avec le symbole d'opérateur `"*"` :
`f"·"x"·"y"·"z = z^(y^(x^f))`
`f"·"(g"·"(h"·"x)) = (hgf)"·"x = ((x^h)^g)^f = x^(hgf)`
ou explicitement :
`f"·"x"·"y"·"z = z"￪"y"￪"x"￪"f`
`f"·"(g"·"(h"·"x)) = (h"*"g"*"f)"·"x = ((x"￪"h)"￪"g)"￪"f = x"￪"(h"*"g"*"f)`
La définition de la composition de fonctions `"*"` à partir de l'opérateur d'application `"￪"`, se note :
`AAfAAgAAx, x^(fg)=(x^f)^g`
ou explicitement :
`AAfAAgAAx, x"￪"(f"*"g)=(x"￪"f)"￪"g`
Remarquez que la priorité syntaxique de l'exposant `"￪"` est à droite d'abord contrairement à la priorité syntaxique du point `"·"` qui est à gauche d'abord. Symétrie oblige, les deux opérateurs ont le même poid syntaxique.
`f"∘"g"∘"h = h"*"g"*"f = hgf`
`f(x)=f"."x=x"￪"f=x^f`
Puisque toute fonction définissable joue le rôle d'un élément distinct et que tout élément joue le rôle d'une fonction distincte, on peut appliquer une fonction sur un argument et appliquer le résultat sur un second argument comme par exemple `f(x)(y)`. Nous pouvons donc définir une fonction binaire `f(".,.")` s'appliquant par exemple à `2` arguments `x,y` comme étant égale à cette expression :
`f(x,y)=f(x)(y)`
Le procédé de curryfication transforme une fonction `f` à plusieurs arguments en une fonction à un seul argument qui retourne une fonction sur le reste des arguments. Le procédé est répété jusqu'à obtenir que des appels de fonction unaire. Exemple de fonction ternaire :
`f(x,y,z)=f(x)(y)(z)`
`f(x,y,z)=f(x,y)(z)`
`f(x,y,z)=f(x)(y,z)`
On ajoute au modèle le shéma d'axiomes de curryfication :
`AAfAAxAAy, f(x,y)=f(x)(y)`
`AAfAAxAAyAAz, f(x,y,z)=f(x)(y)(z)`
`AAfAAxAAyAAzAAt, f(x,y,z,t)=f(x)(y)(z)(t)`
...
Ce shéma d'axiomes définit les fonctions d'arités supérieur à 1.
Toute fonction d'arités supérieur à 1 qui est définissable est associée à un élément. Mais une fois la fonction définie pour une arité particulière, toutes ses arités sont définies.
Une fois la fonction binaire `f(".,.")` définie, celle-ci admet une fonction unaire `f(".")` déterminée comme suit : Lorqu'on l'applique à un élément `x` quelconque elle retourne la fonction `f(x)` qui est définit comme suit : Lorqu'on l'applique à un élément `y` quelconque elle doit retourner `f(x,y)`. Et elle définie complètement la fonction ternaire `f(".,.,.")` qui appliquée à `x,y,z` retourne une fonction `f(x,y,z)` égale au résultat de la fonction `f(x,y)` appliqué à l'élément `z`, noté `f(x,y)(z)`.
Ce shéma d'axiomes ne risque pas de rompre la cohérence du modèle, car l'identifiant d'une fonction est composé de son nom et de son arité. Ainsi, `f(".")` et `f(".,.")` sont considérés comme deux fonctions différentes et libres. On peut donc librement les définir et les lier sans qu'il y ait de conséquence sur la cohérence du modèle. le shéma d'axiomes de curryfication les lie sans occasionner d'incohérence. La définission de l'une des arités d'une fonction définit par curryfication toutes ses autres arités.
Ce shéma d'axiomes de curryfication permet de définir une liste d'arguments sans introduire la liste d'éléments, c'est à dire sans introduire de produit libre que représente l'opérateur virgule dans une liste d'éléments. La liste ne peut pas être produite isolément, elle n'apparait que comme liste d'arguments d'une fonction.
Une autre approche par le langage aboutit au même résultat. On note `a^"*"` l'opérateur `a` pour préciser qu'il peut avoir toutes les arités c'est à dire qu'il peut être un élément `a`, une fonction unaire `a(".")`, une fonction binaire `a(".,.")`, etc., et qu'il retourne un élément. On obtient le langage terminologique multi-aire engendré par quelques opérateurs générateurs par exemple `{a,b,c}`. C'est l'ensemble des compositions d'opérateurs générateurs multi-aire :
`<a^"*",b^"*",c^"*"> = {a,c,a(b),c(a,b),a(b),b(a,c(a)),a(a,b(c(a),c,c))...}`
Puis on considère que l'opérateur multi-aire retourne non pas juste un élément, mais un opérateur également multi-aire que l'on peut alors réappliquer sur une liste d'éléments. On note `a^"∘"` l'opérateur `a` pour préciser qu'il peut avoir toutes les arités et qu'il retourne un opérateur de même type qui peut avoir toutes les arités. On obtient le langage alpha multi-aire :
`<a^"∘",b^"∘",c^"∘"> = {a,a(b),c(a,b)(b),a(b)(a(c))(b,a),a(a,b(c(a)(b))(a))(b,c)...}`
Puis on pose le shéma d'axiomes de curryfication vue plus haut et on obtient le langage alpha unaire.
`<a^"⊙",b^"⊙",c^"⊙"> = {a,c,a(b),c(b(a)),a(b)(c),b(a(c)(a))(b)(a)...}`
Puis on utilise l'opérateur d'application anglais `"·"` que l'on note par absence de symbole juste en juxtaposant l'opérateur et l'opérande, on obtient le langage combinatoire de Curry que l'on appelle simplement « langage alpha» (ne pas confondre avec le langage Alpha, un langage d'optimisations et d'équations proposé dans une thèse en 1989). Dans ce langage, les opérateurs ont une syntaxe préfixée, c'est à dire que l'opérateur est placé à gauche de son opérande et la priorité syntaxique est à gauche d'abord. Les parenthèses n'ont plus qu'un seul rôle celui de prioriser. A titre d'exemples, voici la liste exhaustives des formes jusqu'à 4 variables.
`AAxAAyAAzAAt,`
alpha
alpha unaire
alpha multi-aire`xy` `x(y)` `x(y)` `xyz` `x(y)(z)` `x(y,z)` `x(yz)` `x(y(z))` `x(y(z))` `xyzt` `x(y)(z)(t)` `x(y,z,t)` `x(yzt)` `x(y(z)(t))` `x(y(z,t))` `xy(zt)` `x(y)(z(t))` `x(y,z(t))` `x(yz)t` `x(y(z))(t)` `x(y(z),t)` `x(y(zt))` `x(y(z(t))` `x(y(z(t)))`
Ces langages peuvent être définis avec ou sans le shéma d'axiome de Curryfication. Le langage symétrique existe où les opérateurs ont une syntaxe suffixée c'est à dire que l'opérateur est placé à droite de son opérande et la priorité syntaxique est à droite d'abord.
L'expression `(x"↦"g(f(x),x))` représente une fonction unaire. L'entête est composée d'une nouvelles variable pouvant masquer des variables de même nom déclaré dans le bloc parent, et dont la portée se limite au bloc de définition de la fonction en cours que l'on délimite par des parenthèses. Le corps de la fonction est une expression quelconque tel que ici `g(f(x),x)`. Considérons par exemple :
`H = (x"↦"g(f(x),x))`
La variable dans l'entête désigne une variable libre `x`. La fonction `H` ainsi définie opère comme suit : appliquée à l'élément `a` elle va unifier son entête en substituant dans l'entête comme dans le corps de la fonction, `x` par `a`, et va retourner le corps de la fonction. Ainsi :
`H(a) = g(f(a),a)`
L'expression `((x,y)"↦"g(f(y),x))` représente une fonction binaire. Les variables dans l'entête désigne des variables libres de noms distincts. L'usage de liste d'arguments laisse apparaitre un opérateur de produit libre que joue la virgule dans la liste, mais celui-ci n'existe qu'à l'intérieur des listes d'arguments d'une fonction. Autrement dit, il n'existe qu'à travers l'usage d'une fonction définissable. Grace à la curryfication, la définition d'une fonction `f` d'arité `n` va définir toutes ses autres arités. L'expression `(x"↦"f(x))` désigne la fonction `f`. L'expression `((x,y)"↦"f(x,y))` désigne la même fonction `f` et ainsi de suite :
`f= (x"↦"f(x))`
`f= ((x,y)"↦"f(x,y))`
`f = (x"↦"(y"↦"f(x,y))`
`f= ((x,y,z)"↦"f(x,y,z))`
`f = (x"↦"(y"↦"(z"↦"f(x,y,z)))`
`f= ((x,y)"↦"(z"↦"f(x,y,z)))`
`f= (x"↦"((y,z)"↦"f(x,y,z)))`
L'opération `->` à une priorité syntaxique à droite d'abord. Ainsi par exemple :
`(x"↦"y"↦"z"↦"f(x,y,z)) = (x"↦"(y"↦"(z"↦"f(x,y,z))))`
Le modèle dans ses fondations, avant même sa construction, a défini des opérateurs de syntaxe centrée : `"·","∘","￪","*",` de priorité à gauche d'abord pour `"·"`, et à droite d'abord pour `"￪"`, et associatif pour `"∘"` et `"*"`. Ces opérateurs étant définis, ils sont eux-mêmes des éléments du modèle auxquels on peut appliquer le procédé de curryfication, et les considérer comme des applications unaires. Mais il est plus pratique d'utiliser une syntaxe non-centrée pour faire usage de la currification. En utilisant que des opérateurs de syntaxe préfixée, on définit le "langage alpha".
Haskel Baret Curry (1900 - 1982 logicien américain) présente une liste d'opérateurs de syntaxe préfixée, que l'on présentera d'abord en langage alpha multi-aire, qu'il appelle combinateurs, pour construire un modèle de logique combinatoire. Chaque combinateur est défini classiquement comme une fonction à `n` arguments, par une égalité entre une entête qu'est la fonction appliquée à `n` variables libres de noms distinctes appelée "redex", et un corps qui est une composition quelconque des `n` variables appelé "contractum". Voici quelques premiers opérateurs dont ceux que l'on a définis `"·","∘","￪","*",` et qui correspondent respectivement à `bbI,bbB,bbÇ,bbX` avec une syntaxe préfixée :
`AAxAAyAAf,`
Nom |
Définition multi-aire |
Définition unaire |
Définition en langage alpha |
`bbI` |
`bbI(x)=x` |
`bbI(x)=x` |
`bbIx=x` |
`bbK` |
`bbK(f,x)=f` |
`bbK(f)(x)=f` |
`bbKfx=f` |
`bbÇ` |
`bbÇ(x,f)=f(x)` |
`bbÇ(x)(f)=f(x)` |
`bbÇxf=fx` |
`bbW` |
`bbW(f,x)=f(x,x)` | `bbW(f)(x)=f(x)(x)` | `bbWfx=fx x` |
`bbC` |
`bbC(f,x,y)=f(y,x)` | `bbC(f)(x)(y)=f(y)(x)` | `bbCfxy=fyx` |
`bbB` |
`bbB(f,g,x)=f(g(x))` | `bbB(f)(g)(x)=f(g(x))` | `bbBfgx=f(gx)` |
`bbX` |
`bbX(f,g,x)=g(f(x))` | `bbX(f)(g)(x)=g(f(x))` | `bbXfgx=g(fx)` |
`bbS` |
`bbS(f,g,x)=f(x,g(x))` | `bbS(f)(g)(x)=f(x)(g(x))` | `bbSfgx=fx(gx)` |
| `bbPhi` | `bbPhi(f,g,h,x)=f(g(x),h(x))` | `bbPhi(f)(g)(h)(x)=f(g(x))(h(x))` | `bbPhifghx=f(gx)(hx)` |
| `bbPsi` | `bbPsi(f,g,x,y)=f(g(x),g(y))` | `bbPsi(f)(g)(x)(y)=f(g(x))(g(y))` | `bbPsifgxy=f(gx)(gy)` |
Le premier opérateur le plus simple est l'identité `bbI`. Par currification, `bbI(x,y) = bbI(x)(y)=x(y)`, c'est pourquoi il correspond à l'opérateur d'application anglais `"."` , c'est le même opérateur mais avec une syntaxe préfixée au lieu d'une syntaxe centrée. Notez que les listes ne sont pas des éléments, et donc que l'on ne peut pas définir directrement l'identité binaire puisque l'expression `(x,y)` seule ne constitue pas un élément et n'est pas autorisée. Néanmoins il est possible de la définir comme arguments de toutes les fonctions du modèle, créant ainsi un opérateur `bbDelta` non-curryen, dont il reste à vérifier si son existence ne remet pas en cause la cohérence du modèle :
`AAfAAxAAy, f(bbDelta(x,y))=f(x,y)`
ou en développant :
`AAfAAxAAy, f(bbDelta(x)(y))=f(x)(y)`
Nous étudierons plus-tard les éventuelles contraintes sur le modèle apporté par un tel axiome. Le combinateur appliquant une fonction `f` sur un élément `x` se note `I(f,x)` puisque `I(f,x)=I(f)(x)=f(x)`. Curry définit un certain nombre de combinateurs de base posés avec leur définition ci-dessus : `bbI`, `bbK`, `bbA`, `bbÇ`, `bbW`, `bbC`, `bbB`, `bbX`, `bbS`, `bbPhi`, `bbPsi` où on a ajouté l'opérateur `bbX` correpondant à la composition française des applications. Les combinateurs sont des compositions de combinateurs de base. Par exemple `bbSbbKbbK` est un combinateur, qui comme on le verra, est égale au combinateur `bbI`. La définition du combinateur `bbS` en langage multi-aire est :
`AAfAAgAAx, bbS(f,g,x)=f(x,g(x))`
Sa définition en langage alpha est :
`AAfAAgAAx, bbSfgx=fx(gx)`
Pour utiliser la définiton de `bbS` qui s'applique à 3 arguments, dans le but de simplifier le combinateur `bbSbbKbbK`, on ajoute un argument `x` quantifié universellement au combinateur, `bbSbbKbbKx`. Puis pour procéder à l'élimination du combinateur `bbS`, on procède à l'unification de sa tête `bbSfgx` avec une sous-expression, qui une fois unifié est appelé « redex », et que l'on remplace par son corps `fx(gx)` qui une fois unifié est appelé « contractum » :
`AAx, bbSbbKbbKx`
`= bbKx(bbKx)` (règle d'élimination de `bbS`)
`= x` (règle d'élimination du premier `bbK`)
Donc, grace à l'axiome d'égalité d'application, puisque `AAx, bbSbbKbbKx=bbIx` nous concluons que `bbSbbKbbK=bbI`
On considère un certain nombre de combinateurs de base tel que la liste exposée ci-dessus. Si dans une expression combinatoire apparait un redex, c'est à dire une partie unifiable avec l'entête d'un des combinateurs de base. Celui-ci peut être remplacé par son contractum en substituant les variables du corps du combinateur de base par leur valeur obtenue lors de l'unification de son entête. Les combinateurs de base sont des fonctions qui prennent une liste de variables et les combinent en un arbre applicatif. Donc il est possible dès qu'apparait un combinateur suivi par le nombre d'arguments que nécessite son "arité", de l'effectuer en remplaçant le redex par le contractum. Par Exemple, considérons l'expression combinatoire suivante :
`bbBbbCx(xbbK)y`
On reconnait la sous-expression `bbBbbCx(xbbK)`, appelée redex, qui s'unifie à l'entête du combinateur de base `bbBfgx=f(gx)`. On procède à l'unification (en renommant les variables `f_bbB`, `g_bbB`, `x_bbB` utilisées dans la définition du combinateur de base) `f_bbB"="bbC`, `g_bbB"="x`, `x_bbB"="xbbK`, le corps devient `f_bbB(g_bbB(x)) = C(x(xbbK))` et est appelé le contractum. La réduction se note :
`bbBbbCx(xbbK)y overset(bbB)-> C(x(xbbK))y`
Mais on pouvait aussi reconnaitre la sous-expression `bbCx(xbbK)y` qui s'unifie à l'entête du combinateur de base `bbCfxy=fyx`. On procède à l'unification `f_bbB"="x`, `x_bbB"="xK`, `y_bbB"="y`, le corps devient `f_bbBy_bbBx_bbB = x(xbbK)y`. La réduction se note :
`bbBbbCx(xbbK)y overset(bbC)-> bbBx(xbbK)y`
Puis on reconnait le redex `bbBx(xbbK)y` qui peut être remplacé par le contractum `x((xbbK)x)` que l'on simplifie en `x(xbbKx)`. La réduction se note :
`bbBbbCx(xbbK)y overset(bbC)-> bbBx(xbbK)y overset(bbB)-> x(xbbKx)`
L'expansion est l'opération inverse. Si dans une expression combinatoire apparait un contractum, c'est à dire une partie unifiable avec le corps d'un des combinateurs de base. Celui-ci peut être remplacé par son redex en substituant les variables de l'entête du combinateur de base par leur valeur obtenue lors de l'unification de son corps. L'expansion est noté comme la réduction mais en inversant le sens de la flèche :
`x(xbbKx) overset(bbB)← bbBx(xbbK)y overset(bbC)← bbBbbCx(xbbK)y`
Etant posé une liste de combinateurs générateurs : `bbI`, `bbK`, `bbA`, `bbÇ`, `bbW`, `bbC`, `bbB`, `bbX`, `bbS`, `bbPhi`, `bbPsi`, avec leur définition composé d'une entête listant des variables de noms distincts et un corps. Une expression combinatoire est une composition de combinateurs générateurs et de variables libres quantifiées universellement. L'expression combinatoire est dite irréductible ou dite de forme normal, si elle ne contient aucun redex, c'est à dire si aucune sous-expression n'est unifiable avec l'entête d'un des combinateurs générateurs. Vous constaterez que s'il existe une forme normale, elle est forcement unique parmis toutes celles accessible par réductions et expansions. Par contre certaine expression n'ont pas de forme normale tel que `bbWbbWbbW` qui est un redex produisant la même expression.
Grace à la bijection `varphi` qui associe à chaque fonction définissable de `E` dans `E`, un élément de `E`, tous les éléments se comportent de la même façon. Mais si on s'interdit d'utiliser cette bijection `varphi` ou plutôt si à chaque fois qu'on l'utilise on l'accompagne du changement de type correspondant, alors une distinction déclarative apparait entre les élément de `E` et les fonctions de `E` dans `E`. On définie le type en même temps que le langage de types, récurcivement, comme suit : Les éléments déclarés dans `E` sont de type `E`. Les fonctions déclarées envoyant un élément de type quelconque `alpha` vers un élément de type quelconque `beta` sont de type `alpha->beta`. Les lettres `alpha` et `beta` sont des variables désignant des types quelconques. Le type est donc un arbre nu où les noeud sont l'opérateur `->` et les feuilles sont `E`. La priorité syntaxique de `->` est à droite d'abord, faisant que `E->E->E->E = E->(E->(E->E))`
Si une application `f` est de type `alpha -> beta` et qu'un élément `x` est de type `alpha`, alors `f(x)` sera de type `beta`. En notant les fonctions à l'aide des flèches, on fait apparaître le typage applicatifs :
avec des flêches`x"↦"x` `E->E` `f"↦"x"↦"f` `E->E->E` `x"↦"f"↦"f(x)` `E->(E->E)->E` `x"↦"f"↦"f(x,x)` `E->(E->E->E)->E` `f"↦"x"↦"y"↦"f(y,x)` `(E->E->E)->E->E->E` `f"↦"g"↦"x"↦"f(g(x))` `(E->E)->(E->E)->E->E` `f"↦"g"↦"x"↦"g(f(x))` `(E->E)->(E->E)->E->E` `f"↦"g"↦"x"↦"f(x,g(x))` `(E->E->E)->(E->E)->E->E` `bbPhi` `f"↦"g"↦"h"↦"x"↦"f(g(x),h(x))` `(E->E->E)->(E->E)->(E->E)->E->E` `bbPsi` `f"↦"g"↦"x"↦"y"↦"f(g(x),g(y))` `(E->E->E)->(E->E)->E->E->E`
Dans notre modèle, le type le plus générale `alpha` se définit récurcivement par l'équation `alpha = alpha->alpha`. Il comprend tous les types et représente donc tous les éléments du modèles c'est à dire `E`. L'égalité entre `alpha` et `alpha->alpha` signifie que l'on peut emprunter l'application `varphi` dans un sens ou dans l'autre pour passer de l'élément `E` à la fonction de `E` dans `E` ou réciproquement sans changer de type `alpha`.
Pour pouvoir définir des sous-types, on définit le type le plus générale par seulement une demi-égalité, la posibilité de transformer un élément de `E` en une fonction de `E` dans `E` sans changer de type, mais pas l'inverse. Ce type se définit récursivement par la règle `alpha sup alpha->alpha`. Il existe alors des types récurcifs moins généraux. Les types précédemment listés en sont. Le type le plus générale `E` est définie récurvivement par `E sup E->E`, les autres types sont inclus dans `E`. L'inclusions des types correspond à l'ordre induit par la loi dans le magma monogène `"<"E, ->">"`.
---- 20 mai 2024 ----