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...)

[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.

[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.