[Idée]Lambda-calcul non typé 100% graphique

La palette de composants graphiques :

http://damien-guichard.developpez.co...oppez_0114.png

Il n'y a en tout que trois composants logiques :

1. La boîte-ronde pour l'abstraction.
2. La boîte-coin-arrondi pour l'application. Dans le sens horaire : la fonction, le coin-arrondi puis l'argument.
3. La boîtes-carrée pour les variables. Une boîtes-carrée contient un certain nombre de jetons. Ce nombre n donne la n-ième boîte-ronde rencontrée en suivant le cheminement des flèches. Il désigne l'abstraction par laquelle la variable est liée.

Quelques exemples classiques :

http://damien-guichard.developpez.co...oppez_0115.png

Vous trouvez plus lisible qu'une notation textuelle ? Moins lisible ?
Le principal obstacle concret avant de faire une calculatrice complète c'est l'algo de tree-drawing pour afficher le résultat. Des idées sur ce point ?
:merci:

Bonjour,

Un de mes collègues est très graphes et graphiques pour la représentation du lambda-calcul.

Tu risques de rencontrer un problème lorsque tu auras trop d'applications imbriquées à gauche. Il va sûrement falloir compromettre la proximité des blocs et allonger des flèches, dès lors qu'on attein un niveau supérieur à 3.

L'approche à la de Bruijn rend les choses assez difficile à lire, étiqueter les nœuds par des noms faciliterait la lecture. On connait les problèmes de ce compromis.

Je dirais que je trouve ça :
- moins lisible qu'un texte en nominal ;
- un poil plus lisible qu'un texte en de Bruijn (tant que la taille reste petite).

J'ai tendance à penser que, pour le dessin, tu aurais moins de problème avec une représentation "pyramidale", typique du dessin d'arbres. Ici, le recroquevillement qui s'opère pose problème.

Il y a un bon algo de tree-drawing pyramidal dans La lettre Caml n°5.
Et un algo de β-réduction dans La lettre Caml n°6.
J'ai aussi lu des choses sur la KAM et la G-machine.

Hé bien disons que je me suis laisser distraire un moment par mes jolis petits graphiques (la peur d'affronter mon code OCaml?).

Je ferais bien de retourner à mon projet.
Désolé pour le dérangement.

:arrow: Déplacer n+1 anneaux de la tige A vers la tige C :

Code:

---

1 2 3 4 5 6 7 8 9 10

let rec zfix f x = f (zfix f) x let hanoi hn src tmp dst acc n = if n = 0 then src::dst::acc else hn tmp src dst (src::dst::(hn src dst tmp acc (pred n))) (pred n) let hanoi = (zfix hanoi) 'A' 'B' 'C' []

---

:arrow: Une fois λ-encodé :

Code:

---

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43

let nil = Abs(Abs(Var 1)) let trio = Abs(Abs(Abs(Abs(App(App(App(Var 1,Var 4),Var 3),Var 2))))) let rod_a = Abs(Var 1) let rod_b = Abs(Abs(Var 1)) let rod_c = Abs(Abs(Var 2)) let yfix = Abs(App(Abs(App(Var 2,App(Var 1,Var 1))),Abs(App(Var 2,App(Var 1,Var 1))))) let zero = Abs(Abs(Var 2)) let one = Abs(Abs(App(Var 1,zero))) let two = Abs(Abs(App(Var 1,one))) let three = Abs(Abs(App(Var 1,two))) let hanoi = Abs(Abs(Abs(Abs(Abs(Abs( App( App(Var 1,App(App(App(trio,Var 5),Var 3),Var 2)), (* if n = 0 then src::dst::acc *) Abs( App(App(App(App(App( Var 7, (* hn *) Var 5),(* tmp *) Var 6),(* src *) Var 4),(* dst *) App( App(App(trio,Var 6),Var 4), (* src::dst:: *) App(App(App(App(App(Var 7,Var 6),Var 4),Var 5),Var 3),Var 1) (* hn src dst tmp acc (pred n) *) ) ), Var 1) ) ) )))))) let hanoi = (* yfix hanoi 'A' 'B' 'C' [] *) Abs( App(App(App(App(App( App(yfix,hanoi), rod_a), rod_b), rod_c), nil), Var 1 ) )

---

:arrow: Afin de faciliter le calcul du prédécesseur l'entier pris en paramètre (nombre d'anneaux au départ sur la tige A) est en encodage de Scott.

:arrow: Solution pour 4 anneaux à déplacer de la tige A vers la tige C :

Code:

---

beta_reduction (App(hanoi,three));;

---

:arrow: Comme je n'ai pas encore vérifié la conversion en 2D (l'interpréteur 2D est en cours d'écriture) je me suis contenté d'une apparition furtive (Spoiler Afficher dans ma critique du film TRON Legacy). Si je programme aussi bien en 2D qu'en 1D ça devrait donner quelque chose comme ça :

http://www.aeriesguard.com/var/crypt...orum_large.png

:arrow: J'ai terminé l'écriture de l'interpréteur en 2D. Quelques tests m'ont confirmé que le programme ci-dessus résout bien le jeu des tours de Hanoï.

Ça me motive pour la traduction d'un programme plus conséquent, par exemple :

Code:

---

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22

type function_x = | X | Int of int | Neg of function_x | Sin of function_x | Cos of function_x | Exp of function_x | Power of function_x * int | Add of function_x * function_x | Mul of function_x * function_x let rec deriv = function | X -> Int 1 | Int n -> Int 0 | Neg(u) -> Neg(deriv u) | Sin(u) -> Mul(deriv u,Cos(u)) | Cos(u) -> Neg(Mul(deriv u,Sin(u))) | Exp(u) -> Mul(deriv u,Exp(u)) | Power(u,n) -> Mul(Int n,Mul(deriv u,Power(u,n-1))) | Add(u,v) -> Add(deriv u,deriv v) | Mul(u,v) -> Add(Mul(deriv u,v),Mul(u,deriv v))

---

:arrow: Sur cet exemple les constructeurs (du simple fait de leur nombre) seront considérablement plus abstraits :

Code:

---

1 2 3 4 5 6 7 8 9 10

X ≡ x i n s c e p a m ↦ x Int ≡ j x i n s c e p a m ↦ i j Neg ≡ u x i n s c e p a m ↦ n u Sin ≡ u x i n s c e p a m ↦ s u Cos ≡ u x i n s c e p a m ↦ c u Exp ≡ u x i n s c e p a m ↦ e u Power ≡ u j x i n s c e p a m ↦ p u j Add ≡ u v x i n s c e p a m ↦ a u v Mul ≡ u v x i n s c e p a m ↦ m u v

---

Ça devrait me permettre de mieux appréhender la charge que pose la 2D en matière de contrainte de layout.

:arrow: À gauche la palette de composants taille 39 × 39. À droite la même palette de composants taille 32 × 32. Pour l'un des nombreux éditeurs de cartes à tuiles (comme Mappy) sous win32 ou GTK2.

http://www.aeriesguard.com/var/crypt...orum_large.png http://www.aeriesguard.com/var/crypt...orum_large.png