Discussion :

[davcha]

Suite de ma petite histoire concernant les tests d'églalité entre deux algorithmes, j'ai reprogrammé mon interprêteur de lambda-calcul (vu que j'ai paumé l'autre dans un disque dur qui a cramé... ).

Le fait de l'avoir reprogrammé a été plutôt une bonne chose, dans la mesure où le code est plus robuste et m'a permis de faire des choses un peu plus intéressantes.

Le parseur est capable de reconnaître n'importe quel lambda terme de cette forme : U = x | lambda x°U | (U)U, autrement dit, le parseur est capable de reconnaître n'importe quel lambda-terme "pur".

Afin de simplifier l'écriture des expressions, j'ai réalisé deux "petites" choses : les définitions de terme et les définitions de fonctions.

Une définition de terme s'écrit de la manière suivante : def name°U, avec name, le nom du terme et U le terme associé à la variable.
Par exemple : def vrai ° lambda f°lambda x°f correspond à la définition du terme vrai. On pourra dire que vrai fait alors partie du vocabulaire du langage, puisqu'il s'agit d'un terme défini.
A chaque fois que le parseur rencontrera le mot vrai, il le remplacera par son équivalent en lambda-calcul : lambda f°lambda x°f.

Une définition de fonction est un peu plus complexe que la définition d'un terme.
Je voulais être capable d'écrire une fonction sous n'importe quelle forme.
Par exemple, on écrit souvent un couple en lambda-calcul sous cette forme : (x,y), qui en réalité correspond à ceci : lambda z°((z)x)y.
On écrit souvent, en informatique, les fonctions de cette façon : name(x,y).
Et enfin, pour les opérations mathématiques, on écrit souvent des choses de cette façon : x+y, x*y, x=y...

Il me fallait donc trouver une solution qui prenne en compte toutes les formes d'écritures possibles.

Une fonction se définit donc comme suit : app signature°U, avec signature une "phrase" ponctuée de points d'interrogations (j'avoue m'être inspiré de la façon dont ADO.NET gère les paramètres passés aux requêtes SQL ).

Il devient donc possible d'écrire des choses de ce genre là :

• app (?,?)°lambda a°lambda b°lambda z°((z)a)b, ceci permet ensuite d'utiliser l'expression (x,y) au lieu de lambda z°((z)x)y.
• app if ? then ? else ?°lambda b°lambda u°lambda v°((b)u)v, ceci permet d'utiliser if bool_expr then expr1 else expr2 au lieu de ((bool_expr)expr1)expr2.
• app ?+?°lambda x°lambda y°((x)succ)y, avec succ l'expression successeur en lambda-calcul, ceci permet d'utiliser l'opérateur d'addition plus simplement : a+b à la place de lambda f°lambda x°((a)f)((b)f)x.
• etc...

Ca marche plutôt bien, comme vous pouvez le voir ici : Factorielle(4) - (605 ko) FactoriellePlusRapide(4) - (65 ko).

Cependant, si le moteur régissant les calculs semble fonctionner de façon très correcte, j'ai un petit ennui concernant le parseur.
En effet, en définissant : ?+?, ?*? et ?=?, on ne peut pas écrire de choses de ce genre là : (1+1)*(1+1)=4. Ce qui est plutôt gênant...

Cela vient du fait qu'avec les définitions d'applications, on peut se retrouver avec des symboles qui ne font pas partie, nativement, du lambda-calcul pur.

Explication :
Le parseur prend en paramètre un string, et fait une série de vérifications dessus.

• Il vérifie d'abord si le string est uniquement composé d'une suite ininterrompue de chiffres et de lettres.
  • Si c'est le cas, il vérifie si cette suite appartient aux définitions (def name°U) de l'environnement.
    • Si c'est le cas, il renvoie le lambda-terme correspondant à la définition
    • Sinon, il renvoie le string encapsulé dans un lambda-terme de type variable.
• Sinon, il vérifie si le string est de la forme : lambda x°U.
  • Si c'est le cas, il renvoie un lambda-terme de type abstraction.
• Sinon, il vérifie si le string est composé d'une successions de termes parenthésés.
  • Et c'est là que ça coince.

En effet, quand on envoie le string (1+1)*(1+1) au parseur, le parseur détecte (U)V, avec U = 1+1 et V = *(1+1). Ce qui est évidemment faux, puisqu'il devrait détecter : ?*?.

Mon parseur est donc pour le moment, relativement incorrect, dans la mesure où la gestion des parentèses est assez "foirée".


Si vous avez des idées, ou si vous êtes intéressés... Ou si vous voulez voir le code source du parseur (ça serait sûrement utile pour avoir plus d'idées :p), ça m'aiderait bien en fait.

[DrTopos]

Ton problème tient au fait que les opérateurs * et + sont des opérateurs binaires infixes. Ces opérateurs introduisent de la récursion gauche dans la grammaire. De tels opérateurs ne peuvent être correctement parsés qu'avec un parseur tenant compte de règles de précédence et d'association.

En fait, ce que tu veux parser n'est pas le lamda-calcul pur, mais un extension très large de cette syntaxe. En lambda-calcul pur, il n'y a pas un tel problème de précédences.

Je peux te dire par expérience (car j'ai écrit de nombreux parsers) qu'on peut faire assez facilement un parseur à la main s'il n'y a pas de récursion gauche, mais que cela devient très difficile en présence de récursion gauche. Mon avis est que dans ce cas il faut faire le parser avec un outil comme YACC ou BISON.

[davcha]

Je connais pas du tout Yacc et Bison. J'en ai entendu parlé, évidemment, mais ça s'arrête là.

Et effectivement, je n'aurais logiquement pas ce problème là en lambda-calcul pur, mais bon... le lambda-calcul pur est assez indigeste à lire.

En fait, pour bien faire, je me dis que je devrais peut-être carrément revoir ma façon de voir les choses... Au lieu de jouer avec les expressions régulières et les parenthèses pour détecter les applications, je devrais peut-être carrément réaliser une sorte de parseur de grammaire...

C'est à dire, par exemple...
si j'écris ceci : app if ? then ? else ?°lambda b°lambda u°lambda v°((b)u)v, je lie "if then else" à son équivalent en lambda-calcul...
Mais... Déjà je n'ai aucune information de type, ce qui est normal, tu vas me dire, puisque le lambda-calcul pur n'est pas typé. Mais c'est assez gênant en fait.

En fait je pense à faire une table de correspondances semblable au principe que j'ai amorcé avec "app", mais de pousser ce principe plus loin.
Actuellement, je n'ai que "?" pour dire qu'il y a ici une récursion à faire, mais il serait peut-être intéressant de donner un type à ce "?".

Par exemple : if ?BOOL then ?U else ?U, avec :

• ?BOOL <=> lambda f°lambda x°f OU lambda f°lambda°x
• ?U <=> un lambda terme quelconque

Alors, comment définir ?BOOL et ?U de façon formelle...
Là je m'inspire grossièrement des expressions régulières, mais je traficotte à la sauce "théorie des langages" :

• ?BOOL = (lambda f°lambda x°f | lambda f°lambda x°x)
• ?X = [a-z]
• ?U = (?X | lambda ?X°?U | (?U)?U)

Ca correspond pas mal à la réalité.

Le problème ici, c'est que dans l'expression : if ?BOOL then ?U else ?U, on peut avoir autre chose que du ?U après le then et le else.
Ben oui, ?U est défini, ci-dessus, comme étant un terme du lambda-calcul pur, or on pourrait très bien avoir quelque chose comme ça : if n=0 then 1 else fact(n-1)*n.
Ce qui implique en fait deux choses :

Premièrement, il nous faudrait un type "universel", plus ou moins semblable au type object de c# ou java. On aurait donc quelque chose de ce genre : if ?BOOL then ?object else ?object, qui nous permetterait d'écrire quelque chose comme ceci : if ... then [n'importe quelle instruction] else [n'importe quelle instruction].

Deuxièmement, on voit qu'on a un nouveau problème.
En effet, si j'écris : if n=0 then...., n=0 n'est pas du type ?BOOL. En revanche, n=0 renvoie le type ?BOOL (pour peu que n et 0 soient du type requis par l'opérateur =, dans ce cas précis : entier naturel de church).

Donc, il faut non seulement, si je vois les choses de cette façon que je type mes paramètres formels mais en plus que je type les valeurs de retour des "fonctions" et là je me retrouve avec, en définitive, un langage typé basé sur le lambda-calcul pur.
On aurait donc quelque chose de ce genre :

• app ?BOOL : ?ENC=?ENC
• app ?object : if ?BOOL then ?object else ?object

C'est plutôt chouette je trouve. (?ENC c'est "entier naturel de church)

Par contre, côté perfs, ça risque d'être assez monstrueux...

edit: j'ai oublié de préciser : [n'importe quelle instruction], donc le type ?object serait en fait défini comme "n'importe quel type défini", donc il serait nécessaire que le type en question soit dans la table de correspondances des types.
Par exemple :
Si dans ma table de types, j'ai défini les types suivants : ?bool et ?enc, alors ceci : ?object : if ?bool then ?object else ?object, n'accepterait que des booléens, des entiers naturels de church et une autre instruction if then else.

Ben oui, à ce niveau là, je ne fais pas tellement de différence entre un type et une fonction ou un opérateur.
Je considère en fait que ?bool est une fonction sans paramètres.

[DrTopos]

J'ai un peu de mal à comprendre ta conception des types.

Pourquoi ne pas utiliser directement un lambda-calcul typé, et même un lambda-calcul typé avec couples, pour éviter d'avoir à les simuler avec des lambdas. L'avantage décisif du lambda-calcul typé avec couples est qu'on sait que les évaluations (par beta- et eta- réduction) se terminent toujours (théorème de W.W. Tait).

En ce qui concerne BISON, tu devrais t'y mettre, ne serait-ce que pour la culture. C'est quand même un outil extraordinaire. Quelquechose à connaitre quoi. Il existe sous Linux et sous Windows.

[davcha]

Ca y est, j'ai eu un peu de temps pour me renseigner un peu sur yacc/lex. Je suppose que le principe est identique avec bison/flex ?
C'est vrai que cet outil semble assez merveilleux

En ce qui concerne les types... Il y a quelques temps, dans une autre discussion, je t'avais dit que ma connaissance du lambda-calcul s'arrêtait plus ou moins au lambda-calcul pur (autant dire à la base quoi).
Comme c'est un sujet qui m'intéresse beaucoup (avant tout en tant que loisir ; j'ai pas souvent -- pour pas dire jamais -- l'occasion d'utiliser le lambda-calcul professionnellement), je me renseigne autant que je peux sur ce sujet.
Seulement voilà, ce que j'ai pu lire sur le lambda-calcul typé m'a souvent semblé assez "occulte" (ça explique pourquoi je ne suis pas allé aussi loin pour le moment).

Du coup, quand je me suis retrouvé face au problème que j'expliquais dans ce thread (à savoir : passer d'une expression du genre "if... then... else..." à son équivalent en lambda-calcul, ou inversement), la notion de type telle que je l'ai décrite plus haut m'est venue "toute seule" à l'esprit, naturellement disons.

D'après ce que tu dis "pour éviter d'avoir à les simuler avec des lambdas", j'en déduis qu'un type (quelque soit le système de type choisi), n'est jamais construit de cette manière ? :p


En fait mon idée de départ était de réaliser une sorte de machine virtuelle dont le langage le plus bas niveau aurait été le lambda-calcul pur.
Je me rends compte que cette dernière phrase n'est pas claire du tout, alors je vais faire une analogie.

En ce qui concerne les PC x86, on a le code machine x86 (du code binaire donc), on a un premier niveau d'abstraction qu'est l'assembleur x86, puis on a des langages de plus haut niveau comme le C par exemple.

Le code machine est tout à fait horrible pour l'être humain, mais parfait pour la machine.
L'assembleur est un bon compromis.
Le C (et autres langages de haut niveau) est très lisible pour l'être humain, mais affreux pour la machine.

En fait, dans mon idée de "machine virtuelle en lambda-calcul" :

• le code machine correspond au lambda-calcul pur

exemple (programme) :((lambda m°lambda n°lambda f°lambda x°((m)f)((n)f)x)lambda f°lambda x°(f)(f)x)lambda f°lambda x°(f)(f)(f)x

• l'assembleur correspond à mes "defs"

même exemple (définitions, programme) :
def plus ° lambda m°lambda f°lambda x°((m)f)((n)f)x
def 2 ° lambda f°lambda x°(f)(f)x
def 3 ° lambda f°lambda x°(f)(f)(f)x
((plus)2)3

• le C correspond à mes "apps"

même exemple (définitions, applications, programme) :
def plus ° lambda m°lambda f°lambda x°((m)f)((n)f)x
def 2 ° lambda f°lambda x°(f)(f)x
def 3 ° lambda f°lambda x°(f)(f)(f)x
app ?+? ° plus
2+3

La même chose avec un machine x86 donnerait quelque chose du genre :

• code machine

85EF2DB0....

• assembleur

MOV $x,2
ADD $x,3

• C

int x=2+3;

Et c'est à peu près là qu'est venu naturellement l'idée de typer les applications, puisque l'opérateur + requiert deux entiers de church.

En fait, dans mon esprit, s'il n'y a plus de lien avec le lambda-calcul pur, il n'y a plus de lien non plus avec le "code machine", donc je vois mal comment typer des données sans passer par une définition en lambda-calcul pur.

Par exemple, le type "entier de church", je le noterais bien ainsi :
x,y : variable
O : /*rien*/
T : (x)T | O
lambda x°lambda y°Ty

Mais bon, je devine qu'un type n'est pas du tout construit de cette façon...

[Tellmarch]

En fait dans le typage (enfin un typage simple) associé au lambda calcul, on a des variables de type (qu'on peut noter a, b, c, etc...), puis on construit les types application avec ->.
par exemple le terme "lambda x.x" est typable en "a -> a".

ainsi les types des entiers de church serait N = (a -> a) -> a -> a
alors on peut voir que + est typable avec le type N -> N -> N (c'est à dire qu'à deux entiers on associe un entier.).

Tu pourrais travailler directement avec un systeme de type de ce genre, où les regles de typages sont assez simple à appliquer.

C'est ce qui est fait dans pas mal de langages basés sur le lambda calcul, par exemple dans ocaml (enfin en simplifiant un peu bien sur...)

[davcha]

En fait dans le typage (enfin un typage simple) associé au lambda calcul, on a des variables de type (qu'on peut noter a, b, c, etc...), puis on construit les types application avec ->.
par exemple le terme "lambda x.x" est typable en "a -> a".

Jusqu'ici, ok.

ainsi les types des entiers de church serait N = (a -> a) -> a -> a

Là je ne te suis plus du tout.

alors on peut voir que + est typable avec le type N -> N -> N (c'est à dire qu'à deux entiers on associe un entier.).

Et là je te retrouve, mais ce "+ typé" me semble tellement vague que j'ai la sensation qu'on a perdu toute la notion d'addition là dedans.
Je veux dire que ce + typé pourrait aussi bien être une multiplication, une soustraction, ou même carrément une application qui à deux entiers associe un entier aléatoire qui n'a rien à voir avec les deux précédents entiers.

En fait N -> N -> N pourrait être un type pour n'importe quelle application qui à deux entiers associe un entier, alors je comprends que ça correspond aux prototypes à la signature des fonctions et/ou méthodes en informatique, mais ça s'arrête là... non ?

[Tellmarch]

Là je ne te suis plus du tout.

En gros un entier n prend en argument une fonction de type (a -> a) et une valeur de type a, et renvoie l'itéré n fois de f appliqué à la valeur... d'ou le type que j'ai donné.

Et là je te retrouve, mais ce "+ typé" me semble tellement vague que j'ai la sensation qu'on a perdu toute la notion d'addition là dedans.
Je veux dire que ce + typé pourrait aussi bien être une multiplication, une soustraction, ou même carrément une application qui à deux entiers associe un entier aléatoire qui n'a rien à voir avec les deux précédents entiers.

En fait N -> N -> N pourrait être un type pour n'importe quelle application qui à deux entiers associe un entier, alors je comprends que ça correspond aux prototypes à la signature des fonctions et/ou méthodes en informatique, mais ça s'arrête là... non ?

Euh oui en gros ça correspond à ça... du coup j'ai pas du bien comprendre le probleme dans la discussion en fait, je dois etre hors sujet désolé

[davcha]

Dans ce cas N = (a -> a) -> a -> a, c'est plutôt un type pour les entiers naturels, pas seulement pour les entiers de church, non ?

je dois etre hors sujet désolé

Pas totalement hors sujet

En fait, le problème dans la discussion ici était, au départ, de trouver un bon moyen de parser ce que DrTopos appelait une extension très large de la syntaxe du lambda-calcul pur.
Avec Yacc/Lex je crois avoir trouvé une bonne piste, à ceci près que je devrais être capable de faire ceci à l'exécution, pas à la compilation.

Mais en définitive, ce problème s'inscrit dans un projet plus large, que j'ai expliqué succintement dans un précédent post de ce sujet : réaliser une machine virtuelle se basant sur le lambda-calcul pur.

A la limite, je pourrais me contenter de faire un parseur de lambda calcul pur, mais cela pose le problème d'indigestion de lambdas.
D'où mon histoire de correspondance avec l'assembleur et le C que j'ai expliqué plus avant.

En premier lieu, le but du jeu est d'être capable de transformer une expression "élaborée" en son équivalent en lambda-calcul pur, et également d'effectuer l'opération inverse (qui sera sûrement plus difficile).
Et c'est en fait ici que j'ai besoin des types, tels que je les définis.

Le problème avec N = (a -> a) -> a -> a, si je comprends bien sa signification exacte, est que pour savoir si un terme T est du type N, il va falloir que j'effectue un certain nombre de fois l'opération (a -> a) sur a, dans l'espoir d'obtenir T, ce qui n'est pas certain.
En fait, si je ne dis pas de bétise, N = (a -> a) -> a -> a, peut correspondre à la construction récursive des entiers naturels : (F(n),0) -> n+1 ?
Si c'est bien le cas, alors pour vérifier que T est de type N, je dois effectuer la récursion à partir de 0 jusqu'à ce que je tombe sur T, mais si T n'est pas de type N, alors cette opération de vérification ne se terminera, à priori, jamais. J'ai bon ou j'oublie quelque chose ?

Avec la construction des entiers de church suivante :
x,y : variable
R = (x)R | /*rien*/
N = lambda x°lambda y°Rx
Je suis certain que l'opération répondant à la question "T est-il de type N ?" finira.

Je me trompe ou je dis n'importe quoi ?

[Tellmarch]

D'accord je crois que j'ai compris ce que tu voulais faire...

Dans ce cas N = (a -> a) -> a -> a, c'est plutôt un type pour les entiers naturels, pas seulement pour les entiers de church, non ?

Non il s'agit bien du type des entiers de church, tous les termes de la forme λfx.(f(f(f x))) seront de ce type là, mais on ne peut pas representer des entiers négatifs avec ce type je pense.

Le problème avec N = (a -> a) -> a -> a, si je comprends bien sa signification exacte, est que pour savoir si un terme T est du type N, il va falloir que j'effectue un certain nombre de fois l'opération (a -> a) sur a, dans l'espoir d'obtenir T, ce qui n'est pas certain.
En fait, si je ne dis pas de bétise, N = (a -> a) -> a -> a, peut correspondre à la construction récursive des entiers naturels : (F(n),0) -> n+1 ?
Si c'est bien le cas, alors pour vérifier que T est de type N, je dois effectuer la récursion à partir de 0 jusqu'à ce que je tombe sur T, mais si T n'est pas de type N, alors cette opération de vérification ne se terminera, à priori, jamais. J'ai bon ou j'oublie quelque chose ?

Le typage des termes de λ-calcul ne fonctionne pas vraiment comme ça. On applique des regles de typage générales, non spécifiques au entiers... Par exemple le terme λx.x est typable en a -> a, mais pas en le type (a -> a) -> a -> a, donc ça ne sera pas interprété comme un entier.

Avec la construction des entiers de church suivante :
x,y : variable
R = (x)R | /*rien*/
N = lambda x°lambda y°Rx
Je suis certain que l'opération répondant à la question "T est-il de type N ?" finira.

Je me trompe ou je dis n'importe quoi ?

Un probleme possible dans ce que tu proposes est le cas où tu as un terme non entierement beta réduit par exemple...
Le terme λfx.(λy.x)(xx) est bien β-équivalent à l'entier de church 0, mais ton outil ne le détecterait pas comme un nombre. (Au passage tu n'utilises pas la convention de parenthésage usuelle pour le lambda calcul, mais bon c'est un détail sans doute)
Je ne sais pas trop si c'est un réel probleme pour ce que tu veux faire toi, mais en tout cas les langages basés sur le lambda calcul n'utilisent pas un systeme de type tel que tu le définis toi, mais plutot un systeme de type basé (mais en plus évolué) sur le typage usuel du lambda calcul (le typage "à la curry", c'est à dire en gros celui que j'ai définit plus haut).

[davcha]

Non il s'agit bien du type des entiers de church, tous les termes de la forme λfx.(f(f(f x))) seront de ce type là, mais on ne peut pas representer des entiers négatifs avec ce type je pense.

J'ai parlé d'entiers naturels, pas relatifs :p
Je me dis qu'il y a sûrement d'autres façon de représenter, en lambda calcul, les entiers naturels, qu'avec les entiers de church.
Et lambda m°lambda f°lambda x°((m)f)(f)x requiert, précisément, les entiers de church. D'où mon étonnement sur ce typage.

Le typage des termes de λ-calcul ne fonctionne pas vraiment comme ça. On applique des regles de typage générales, non spécifiques au entiers... Par exemple le terme λx.x est typable en a -> a, mais pas en le type (a -> a) -> a -> a, donc ça ne sera pas interprété comme un entier.

Ce qui m'ennuie avec ce typage là, c'est, par exemple, qu'un type (a -> a) -> a -> a n'est pas exclusivement un type pour les entiers, mais est en réalité un type valable pour n'importe quelle suite de termes, je me trompe ?

Un probleme possible dans ce que tu proposes est le cas où tu as un terme non entierement beta réduit par exemple...
Le terme λfx.(λy.x)(xx) est bien β-équivalent à l'entier de church 0, mais ton outil ne le détecterait pas comme un nombre. (Au passage tu n'utilises pas la convention de parenthésage usuelle pour le lambda calcul, mais bon c'est un détail sans doute)

Oui, c'est vrai. Mon outil ne fonctionnerait correctement que pour les termes normalisés.
Par contre, j'utilise le parenthèsage à gauche, celui opté pour J.L.Krivine.

Je ne sais pas trop si c'est un réel probleme pour ce que tu veux faire toi, mais en tout cas les langages basés sur le lambda calcul n'utilisent pas un systeme de type tel que tu le définis toi, mais plutot un systeme de type basé (mais en plus évolué) sur le typage usuel du lambda calcul (le typage "à la curry", c'est à dire en gros celui que j'ai définit plus haut).

En fait les deux sont intéressants, je trouve.

[Jean-Marc.Bourguet]

Je peux te dire par expérience (car j'ai écrit de nombreux parsers) qu'on peut faire assez facilement un parseur à la main s'il n'y a pas de récursion gauche, mais que cela devient très difficile en présence de récursion gauche.

Si les récursions à gauche ne font que gérer l'associativité (comme c'est apparemment le cas ici), ce n'est pas un problème.

[Jean-Marc.Bourguet]

Ca y est, j'ai eu un peu de temps pour me renseigner un peu sur yacc/lex. Je suppose que le principe est identique avec bison/flex ?
C'est vrai que cet outil semble assez merveilleux

bison est une réimplémentation de yacc, avec des extensions.

flex est aussi une réimplémentation de lex, et je crois que c'est la seule utilisée de nos jours (pour yacc, il y a aussi byacc).

Le problème principal des générateurs de parseurs, c'est la qualité abyssimale de la gestion des erreurs.

Le second problème, c'est que c'est bien pour des grammaires qui ont été conçues en fonction de leurs limitations. Si ce n'est pas le cas (C, C++, VHDL pour citer trois cas que je connais) utiliser ces outils devient du sport et un parseur écrit à la main est plus facile à utiliser.

Le gros avantage, c'est la facilté d'utilisation, en particulier dans les contextes où on maîtrise la syntaxe (donc où le second problème n'en est pas un) et que celle-ci est toujours en évolution.

[Tellmarch]

bison est une réimplémentation de yacc, avec des extensions.

flex est aussi une réimplémentation de lex, et je crois que c'est la seule utilisée de nos jours (pour yacc, il y a aussi byacc).

Il y a aussi ocamllex et ocamlyacc