(I) (0) JE MONTE ---->(0) COMBINATEUR INVERSIBLE VOICI L INVERSE: ----> (I) VOULEZ-VOUS VERIFIER? ? non = OK ; time = 319 ms. ;? (ci (c)) <—– le combinateur C
(C) (0 2 1) JE MONTE ---->(0 2 1) COMBINATEUR INVERSIBLE VOICI L INVERSE: ----> (C) VOULEZ-VOUS VERIFIER? ? non = OK ; time = 410 ms. ;? (ci (b)) <—– le combinateur B
(B) (0 (1 2)) = (PAS DE COMBINATEUR EN DEBUT DE LISTE) ; time = 83 ms. ;? (ci (w)) <—– le combinateur W
(W) (0 1 1) JE MONTE ---->(0 1 1) = (IL Y A UNE SUITE DE VARIABLES QUI N 'EST PAS UNE PERMUTATION) ; time = 142 ms. ;? (ci (k)) <—– le combinateur K
(K) (0) JE MONTE ---->(0) = (IL Y A UNE SUITE DE VARIABLES QUI N 'EST PAS UNE PERMUTATION) ; time = 82 ms. ;? (ci (s)) <—– le combinateur S
(S) (0 2 (1 2)) = (PAS DE COMBINATEUR EN DEBUT DE LISTE) ; time = 78 ms. ;les différents déguisements de C examinés précédemment.
(B (C (C (B (B (B (B C) B)) C) C) K) B) (C (C (B (B (B (B C) B)) C) C) K (B 0)) (C (B (B (B (B C) B)) C) C (B 0) K) (B (B (B (B C) B)) C (B 0) C K) (B (B (B C) B) (C (B 0)) C K) (B (B C) B (C (B 0) C) K) (B C (B (C (B 0) C)) K) (C (B (C (B 0) C) K)) (B (C (B 0) C) K 2 1) (C (B 0) C (K 2) 1) (B 0 (K 2) C 1) (0 (K 2 C) 1) JE DESCENDS ----> (K 2 C) FAUT FAIRE UNE ABSTRACTION JE M EN OCCUPE VOILA ----> (C K C 2) JE DESCENDS ----> (C K C 2) (K 0 C) (0) JE MONTE ---->(0) 1 JE MONTE ---->(0 2 (0) 1) COMBINATEUR INVERSIBLE VOICI L INVERSE: ----> (C) VOULEZ-VOUS VERIFIER? ? non = OK ; time = 2329 ms. ;? (ci (b(c(b(b(c(b c)c)b))c)b)) <—–C2
(B (C (B (B (C (B C) C) B)) C) B) (C (B (B (C (B C) C) B)) C (B 0)) (B (B (C (B C) C) B) (B 0) C) (B (C (B C) C) B (B 0 C)) (C (B C) C (B (B 0 C))) (B C (B (B 0 C)) C) (C (B (B 0 C) C)) (B (B 0 C) C 2 1) (B 0 C (C 2) 1) (0 (C (C 2)) 1) JE DESCENDS ----> (C (C 2)) FAUT FAIRE UNE ABSTRACTION JE M EN OCCUPE VOILA ----> (B C C 2) JE DESCENDS ----> (B C C 2) (C (C 0)) (C 0 2 1) (0 1 2) JE MONTE ---->(0 1 2) 1 JE MONTE ---->(0 2 (0 1 2) 1) COMBINATEUR INVERSIBLE VOICI L INVERSE: ----> (C) VOULEZ-VOUS VERIFIER? ? non = OK ; time = 2179 ms. ;? (ci (b(c(b c)(c b i))b)) <—– C3
(B (C (B C) (C B I)) B) (C (B C) (C B I) (B 0)) (B C (B 0) (C B I)) (C (B 0 (C B I))) (B 0 (C B I) 2 1) (0 (C B I 2) 1) JE DESCENDS ----> (C B I 2) (B 0 I) (0 (I 1)) JE DESCENDS ----> (I 1) (0) JE MONTE ---->(0) NIL JE MONTE ---->(0 1 (0)) 1 JE MONTE ---->(0 2 (0 1 (0)) 1) COMBINATEUR INVERSIBLE VOICI L INVERSE: ----> (C) VOULEZ-VOUS VERIFIER? ? non = OK ; time = 1781 ms. ;? (ci (b(b(b c(c b k))(b w))b)) <—– C4
(B (B (B C (C B K)) (B W)) B) (B (B C (C B K)) (B W) (B 0)) (B C (C B K) (B W (B 0))) (C (C B K (B W (B 0)))) (C B K (B W (B 0)) 2 1) (B (B W (B 0)) K 2 1) (B W (B 0) (K 2) 1) (W (B 0 (K 2)) 1) (B 0 (K 2) 1 1) (0 (K 2 1) 1) FAUT ESSAYER DE METTRE EN FORME NORMALE (2) (2) JE MONTE ---->(0 2 1) COMBINATEUR INVERSIBLE VOICI L INVERSE: ----> (C) VOULEZ-VOUS VERIFIER? ? non = OK ; time = 1497 ms. ;? (ci (c(c(b(b(b(b(b(b w)b))b)(b c))b)(c b))(k i))) <—– C5
(C (C (B (B (B (B (B (B W) B)) B) (B C)) B) (C B)) (K I)) (C (B (B (B (B (B (B W) B)) B) (B C)) B) (C B) 0 (K I)) (B (B (B (B (B (B W) B)) B) (B C)) B 0 (C B) (K I)) (B (B (B (B (B W) B)) B) (B C) (B 0) (C B) (K I)) (B (B (B (B W) B)) B (B C (B 0)) (C B) (K I)) (B (B (B W) B) (B (B C (B 0))) (C B) (K I)) (B (B W) B (B (B C (B 0)) (C B)) (K I)) (B W (B (B (B C (B 0)) (C B))) (K I)) (W (B (B (B C (B 0)) (C B)) (K I))) (B (B (B C (B 0)) (C B)) (K I) 1 1) (B (B C (B 0)) (C B) (K I 1) 1) (B C (B 0) (C B (K I 1)) 1) (C (B 0 (C B (K I 1))) 1) (B 0 (C B (K I 1)) 2 1) (0 (C B (K I 1) 2) 1) FAUT ESSAYER DE METTRE EN FORME NORMALE (B 2 (K I 1)) (I) (B 2 (I)) JE DESCENDS ----> (B 2 (I)) FAUT FAIRE UNE ABSTRACTION JE M EN OCCUPE VOILA ----> (C B (I) 2) JE DESCENDS ----> (C B (I) 2) (B 0 I) (0 (I 1)) JE DESCENDS ----> (I 1) (0) JE MONTE ---->(0) NIL JE MONTE ---->(0 1 (0)) 1 JE MONTE ---->(0 2 (0 1 (0)) 1) COMBINATEUR INVERSIBLE VOICI L INVERSE: ----> (C) VOULEZ-VOUS VERIFIER? ? oui VOTRE COMBINATEUR ----> (C (C (B (B (B (B (B (B W) B)) B) (B C)) B) ( C B)) (K I)) SON INVERSE ----> (C) (B (C (C (B (B (B (B (B (B W) B)) B) (B C)) B) (C B)) (K I)) C) (C (C (B (B (B (B (B (B W) B)) B) (B C)) B) (C B)) (K I) (C 0)) (C (B (B (B (B (B (B W) B)) B) (B C)) B) (C B) (C 0) (K I)) (B (B (B (B (B (B W) B)) B) (B C)) B (C 0) (C B) (K I)) (B (B (B (B (B W) B)) B) (B C) (B (C 0)) (C B) (K I)) (B (B (B (B W) B)) B (B C (B (C 0))) (C B) (K I)) (B (B (B W) B) (B (B C (B (C 0)))) (C B) (K I)) (B (B W) B (B (B C (B (C 0))) (C B)) (K I)) (B W (B (B (B C (B (C 0))) (C B))) (K I)) (W (B (B (B C (B (C 0))) (C B)) (K I))) (B (B (B C (B (C 0))) (C B)) (K I) 1 1) (B (B C (B (C 0))) (C B) (K I 1) 1) (B C (B (C 0)) (C B (K I 1)) 1) (C (B (C 0) (C B (K I 1))) 1) (B (C 0) (C B (K I 1)) 2 1) (C 0 (C B (K I 1) 2) 1) (0 1 (C B (K I 1) 2)) FAUT ESSAYER DE METTRE EN FORME NORMALE (B 2 (K I 1)) (I) (B 2 (I)) JE DESCENDS ----> (B 2 (I)) FAUT FAIRE UNE ABSTRACTION JE M EN OCCUPE VOILA ----> (C B (I) 2) JE DESCENDS ----> (C B (I) 2) (B 0 I) (0 (I 1)) JE DESCENDS ----> (I 1) (0) JE MONTE ---->(0) NIL JE MONTE ---->(0 1 (0)) NIL JE MONTE ---->(0 1 2 (0 1 (0))) = (VOILA VOUS RECONNAISSEZ L 'IDENTITE) ; time = 8573 ms. ;voici un permutateur héréditairement fini, donc inversible,avec 9 niveaux d'imbrications de sous termes.
? super3 = (C B (C B (C B (C B (C B (C B (C B (C B (C B (B C (B C))))))))))) ; time = 0 ms. ;? (ci super3)
(B 0 (C B (C B (C B (C B (C B (C B (C B (C B (B C (B C))))))))))) (0 (C B (C B (C B (C B (C B (C B (C B (C B (B C (B C))))))))) 1)) JE DESCENDS ----> (C B (C B (C B (C B (C B (C B (C B (C B (B C (B C) )))))))) 1) (B 0 (C B (C B (C B (C B (C B (C B (C B (B C (B C)))))))))) (0 (C B (C B (C B (C B (C B (C B (C B (B C (B C)))))))) 1)) JE DESCENDS ----> (C B (C B (C B (C B (C B (C B (C B (B C (B C)))))) )) 1) (B 0 (C B (C B (C B (C B (C B (C B (B C (B C))))))))) (0 (C B (C B (C B (C B (C B (C B (B C (B C))))))) 1)) JE DESCENDS ----> (C B (C B (C B (C B (C B (C B (B C (B C))))))) 1) (B 0 (C B (C B (C B (C B (C B (B C (B C)))))))) (0 (C B (C B (C B (C B (C B (B C (B C)))))) 1)) JE DESCENDS ----> (C B (C B (C B (C B (C B (B C (B C)))))) 1) (B 0 (C B (C B (C B (C B (B C (B C))))))) (0 (C B (C B (C B (C B (B C (B C))))) 1)) JE DESCENDS ----> (C B (C B (C B (C B (B C (B C))))) 1) (B 0 (C B (C B (C B (B C (B C)))))) (0 (C B (C B (C B (B C (B C)))) 1)) JE DESCENDS ----> (C B (C B (C B (B C (B C)))) 1) (B 0 (C B (C B (B C (B C))))) (0 (C B (C B (B C (B C))) 1)) JE DESCENDS ----> (C B (C B (B C (B C))) 1) (B 0 (C B (B C (B C)))) (0 (C B (B C (B C)) 1)) JE DESCENDS ----> (C B (B C (B C)) 1) (B 0 (B C (B C))) (0 (B C (B C) 1)) JE DESCENDS ----> (B C (B C) 1) (C (B C 0)) (B C 0 2 1) (C (0 2) 1) (0 2 3 1) JE MONTE ---->(0 2 3 1) NIL JE MONTE ---->(0 1 (0 2 3 1)) NIL JE MONTE ---->(0 1 (0 1 (0 2 3 1))) NIL JE MONTE ---->(0 1 (0 1 (0 1 (0 2 3 1)))) NIL JE MONTE ---->(0 1 (0 1 (0 1 (0 1 (0 2 3 1))))) NIL JE MONTE ---->(0 1 (0 1 (0 1 (0 1 (0 1 (0 2 3 1)))))) NIL JE MONTE ---->(0 1 (0 1 (0 1 (0 1 (0 1 (0 1 (0 2 3 1))))))) NIL JE MONTE ---->(0 1 (0 1 (0 1 (0 1 (0 1 (0 1 (0 1 (0 2 3 1)))))))) NIL JE MONTE ---->(0 1 (0 1 (0 1 (0 1 (0 1 (0 1 (0 1 (0 1 (0 2 3 1))))))) )) NIL JE MONTE ---->(0 1 (0 1 (0 1 (0 1 (0 1 (0 1 (0 1 (0 1 (0 1 (0 2 3 1)) )))))))) COMBINATEUR INVERSIBLE VOICI L INVERSE: ----> (C B (C B (C B (C B (C B (C B (C B (C B (C B (B (B C) C)))))))) )) VOULEZ-VOUS VERIFIER? ? non = OK ; time = 16457 ms. ;un autre exemple intéressant
? super4 = (C (B (B C) B) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C)) ; time = 0 ms. ;? (ci super4)
(B (B C) B 0 (C (C (B (B (B B C)) B) (C B (B C (B C)))) C)) (B C (B 0) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C)) (C (B 0 (C (C (B (B (B B C)) B) (C B (B C (B C)))) C))) (B 0 (C (C (B (B (B B C)) B) (C B (B C (B C)))) C) 2 1) (0 (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 2) 1) JE DESCENDS ----> (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 2) (C (B (B (B B C)) B) (C B (B C (B C))) 0 C) (B (B (B B C)) B 0 (C B (B C (B C))) C) (B (B B C) (B 0) (C B (B C (B C))) C) (B B C (B 0 (C B (B C (B C)))) C) (B (C (B 0 (C B (B C (B C))))) C) (C (B 0 (C B (B C (B C)))) (C 1)) (B 0 (C B (B C (B C))) 2 (C 1)) (0 (C B (B C (B C)) 2) (C 1)) JE DESCENDS ----> (C B (B C (B C)) 2) (B 0 (B C (B C))) (0 (B C (B C) 1)) JE DESCENDS ----> (B C (B C) 1) (C (B C 0)) (B C 0 2 1) (C (0 2) 1) (0 2 3 1) JE MONTE ---->(0 2 3 1) NIL JE MONTE ---->(0 1 (0 2 3 1)) (C 1) JE DESCENDS ----> (C 1) (0 2 1) JE MONTE ---->(0 2 1) NIL JE MONTE ---->(0 2 (0 1 (0 2 3 1)) 1 (0 2 1)) 1 JE MONTE ---->(0 2 (0 2 (0 1 (0 2 3 1)) 1 (0 2 1)) 1) COMBINATEUR INVERSIBLE VOICI L INVERSE: ----> (C (B B C) (C (C (B (B (B B C)) B) C) (C B (B (B C) C)))) VOULEZ-VOUS VERIFIER? ? oui VOTRE COMBINATEUR ----> (C (B (B C) B) (C (C (B (B (B B C)) B) (C B ( B C (B C)))) C)) SON INVERSE ----> (C (B B C) (C (C (B (B (B B C)) B) C) (C B (B (B C) C)))) (B (C (B (B C) B) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C)) (C ( B B C) (C (C (B (B (B B C)) B) C) (C B (B (B C) C))))) (C (B (B C) B) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C) (C (B B C) (C (C (B (B (B B C)) B) C) (C B (B (B C) C))) 0)) (B (B C) B (C (B B C) (C (C (B (B (B B C)) B) C) (C B (B (B C) C))) 0 ) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C)) (B C (B (C (B B C) (C (C (B (B (B B C)) B) C) (C B (B (B C) C))) 0)) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C)) (C (B (C (B B C) (C (C (B (B (B B C)) B) C) (C B (B (B C) C))) 0) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C))) (B (C (B B C) (C (C (B (B (B B C)) B) C) (C B (B (B C) C))) 0) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C) 2 1) (C (B B C) (C (C (B (B (B B C)) B) C) (C B (B (B C) C))) 0 (C (C (B ( B (B B C)) B) (C B (B C (B C)))) C 2) 1) (B B C 0 (C (C (B (B (B B C)) B) C) (C B (B (B C) C))) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 2) 1) (B (C 0) (C (C (B (B (B B C)) B) C) (C B (B (B C) C))) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 2) 1) (C 0 (C (C (B (B (B B C)) B) C) (C B (B (B C) C)) (C (C (B (B (B B C) ) B) (C B (B C (B C)))) C 2)) 1) (0 1 (C (C (B (B (B B C)) B) C) (C B (B (B C) C)) (C (C (B (B (B B C) ) B) (C B (B C (B C)))) C 2))) JE DESCENDS ----> (C (C (B (B (B B C)) B) C) (C B (B (B C) C)) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 2)) FAUT FAIRE UNE ABSTRACTION JE M EN OCCUPE VOILA ----> (B (C (C (B (B (B B C)) B) C) (C B (B (B C) C))) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C) 2) JE DESCENDS ----> (B (C (C (B (B (B B C)) B) C) (C B (B (B C) C))) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C) 2) (C (C (B (B (B B C)) B) C) (C B (B (B C) C)) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 0)) (C (B (B (B B C)) B) C (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 0 ) (C B (B (B C) C))) (B (B (B B C)) B (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 0) C (C B (B (B C) C))) (B (B B C) (B (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 0)) C (C B (B (B C) C))) (B B C (B (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 0) C) (C B (B (B C) C))) (B (C (B (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 0) C)) (C B (B (B C) C))) (C (B (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 0) C) (C B (B (B C ) C) 1)) (B (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 0) C 2 (C B (B (B C) C) 1)) (C (C (B (B (B B C)) B) (C B (B C (B C)))) C 0 (C 2) (C B (B (B C) C) 1)) (C (B (B (B B C)) B) (C B (B C (B C))) 0 C (C 2) (C B (B (B C) C) 1)) (B (B (B B C)) B 0 (C B (B C (B C))) C (C 2) (C B (B (B C) C) 1)) (B (B B C) (B 0) (C B (B C (B C))) C (C 2) (C B (B (B C) C) 1)) (B B C (B 0 (C B (B C (B C)))) C (C 2) (C B (B (B C) C) 1)) (B (C (B 0 (C B (B C (B C))))) C (C 2) (C B (B (B C) C) 1)) (C (B 0 (C B (B C (B C)))) (C (C 2)) (C B (B (B C) C) 1)) (B 0 (C B (B C (B C))) (C B (B (B C) C) 1) (C (C 2))) (0 (C B (B C (B C)) (C B (B (B C) C) 1)) (C (C 2))) JE DESCENDS ----> (C B (B C (B C)) (C B (B (B C) C) 1)) FAUT FAIRE UNE ABSTRACTION JE M EN OCCUPE VOILA ----> (B (C B (B C (B C))) (C B (B (B C) C)) 1) JE DESCENDS ----> (B (C B (B C (B C))) (C B (B (B C) C)) 1) (C B (B C (B C)) (C B (B (B C) C) 0)) (B (C B (B (B C) C) 0) (B C (B C))) (C B (B (B C) C) 0 (B C (B C) 1)) (B 0 (B (B C) C) (B C (B C) 1)) (0 (B (B C) C (B C (B C) 1))) JE DESCENDS ----> (B (B C) C (B C (B C) 1)) FAUT FAIRE UNE ABSTRACTION JE M EN OCCUPE VOILA ----> (B (B (B C) C) (B C (B C)) 1) JE DESCENDS ----> (B (B (B C) C) (B C (B C)) 1) (B (B C) C (B C (B C) 0)) (B C (C (B C (B C) 0))) (C (C (B C (B C) 0) 1)) (C (B C (B C) 0) 1 3 2) (B C (B C) 0 3 1 2) (C (B C 0) 3 1 2) (B C 0 1 3 2) (C (0 1) 3 2) (0 1 2 3) JE MONTE ---->(0 1 2 3) NIL JE MONTE ---->(0 1 (0 1 2 3)) (C (C 2)) JE DESCENDS ----> (C (C 2)) FAUT FAIRE UNE ABSTRACTION JE M EN OCCUPE VOILA ----> (B C C 2) JE DESCENDS ----> (B C C 2) (C (C 0)) (C 0 2 1) (0 1 2) JE MONTE ---->(0 1 2) NIL JE MONTE ---->(0 1 (0 1 (0 1 2 3)) 2 (0 1 2)) NIL JE MONTE ---->(0 1 2 (0 1 (0 1 (0 1 2 3)) 2 (0 1 2))) = (VOILA VOUS RECONNAISSEZ L 'IDENTITE) ; time = 25286 ms. ;voici deux combinateurs sans forme normale qui ne font pas boucler l'algorithme.
(C (B C (C I)) (W W W)) (B C (C I) 0 (W W W)) (C (C I 0) (W W W)) (C I 0 1 (W W W)) (I 1 0 (W W W)) (1 0 (W W W)) = (PAS REGULIER) ; time = 459 ms. ;? (ci (c c(w w w)))
(C C (W W W)) (C 0 (W W W)) (0 1 (W W W)) = (PAS DE VARIABLE DANS UN SOUS TERME) ; time = 221 ms. ;en voici un sans forme normale qui le fait boucler.
(C (B C (B B)) (W W W)) (B C (B B) 0 (W W W)) (C (B B 0) (W W W)) (B B 0 1 (W W W)) (B (0 1) (W W W)) (0 1 (W W W 2)) JE DESCENDS ----> (W W W 2) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W) (W W W)voici pour terminer et arrêter le suspens introduit au début de ce chapitre le premier exemple présenté.
(B (B (C B C) (B (C (B (B (C (B B C) C)) B) C))) C) (B (C B C) (B (C (B (B (C (B B C) C)) B) C)) (C 0)) (C B C (B (C (B (B (C (B B C) C)) B) C) (C 0))) (B (B (C (B (B (C (B B C) C)) B) C) (C 0)) C) (B (C (B (B (C (B B C) C)) B) C) (C 0) (C 1)) (C (B (B (C (B B C) C)) B) C (C 0 (C 1))) (B (B (C (B B C) C)) B (C 0 (C 1)) C) (B (C (B B C) C) (B (C 0 (C 1))) C) (C (B B C) C (B (C 0 (C 1)) C)) (B B C (B (C 0 (C 1)) C) C) (B (C (B (C 0 (C 1)) C)) C) (C (B (C 0 (C 1)) C) (C 2)) (B (C 0 (C 1)) C 3 (C 2)) (C 0 (C 1) (C 3) (C 2)) (0 (C 3) (C 1) (C 2)) JE DESCENDS ----> (C 3) (0 2 1) JE MONTE ---->(0 2 1) (C 1) JE DESCENDS ----> (C 1) (0 2 1) JE MONTE ---->(0 2 1) (C 2) JE DESCENDS ----> (C 2) (0 2 1) JE MONTE ---->(0 2 1) NIL JE MONTE ---->(0 3 (0 2 1) 1 (0 2 1) 2 (0 2 1)) COMBINATEUR INVERSIBLE VOICI L INVERSE: ----> (C (C (C (B (B (B (B (B (B B C)) C)) B) (B (B (B C) B))) C) C) C) VOULEZ-VOUS VERIFIER? ? non = OK