D'accord, si je comprend bien, passer une continuation c'est éviter de faire la preuve maintenant, et la passer en argument du reste de la preuve pour l'instancier quand on en a besoin (ce qui se passe aux branches des preuves généralement).
Mais j'ai alors un problème, parce que le principe du modus-ponens est tout de même dans le calcul des séquents classique sans coupures : on a une règle (gauche)
G, B |- D G,A |- B,D
-------------------------- =>-gauche
G, A => B |- D
Ce n'est pas exactement une coupure, mais cela fait bien deux évaluations et donc conserve la nécessité de garder une pile d'appel pour l'évaluation. Par exemple cette règle semble nécessaire pour prouver ((A=>B)=>A)=>(A=>A))
[^] # Re: Programmation Dynamique
Posté par Aluminium95 . En réponse au journal Haskell -- Évaluation paresseuse. Évalué à 1.
D'accord, si je comprend bien, passer une continuation c'est éviter de faire la preuve maintenant, et la passer en argument du reste de la preuve pour l'instancier quand on en a besoin (ce qui se passe aux branches des preuves généralement).
Mais j'ai alors un problème, parce que le principe du modus-ponens est tout de même dans le calcul des séquents classique sans coupures : on a une règle (gauche)
Ce n'est pas exactement une coupure, mais cela fait bien deux évaluations et donc conserve la nécessité de garder une pile d'appel pour l'évaluation. Par exemple cette règle semble nécessaire pour prouver
((A=>B)=>A)=>(A=>A))