Résumé des traductions CPS des opérateurs de contrôle délimités
---------------------------------------------------------------
Rédigé en octobre 2011

*** CPS traduction double de Danvy-Filinski ***

X +                  = X
A_T->B_U +           = (~U -> ~B+) -> (~T -> ~A+)
Gamma |- V:A +       = Gamma+ |- V+ : A+
Gamma, T |- M:A, U + = Gamma+ |- M* : (~T -> ~A+) -> ~~U

x +        =  x
\x.M +     =  \k.\K.\x.(M* k K)
V *        =  \k.\K.(k K V+)
M N *      =  \k.(M* \K.\m.(N* (m k) K))
           =  \k.(M* \K.\m.(N* \n.(m k n) K))

S +        =  \k.\K.\x.(x \K.K K (\k'.\K'.(k (k' K'))))
           =  \k.\K.\x.(x \K.K K (\k'.\K'.\v.(k \w.(k' K' w) v)))
<M> *      =  \k.\K.(M* \K.K (k K))

C +        =  \k.\K.\x.(x \K.K K (\_.k))
           =  \k.\K.\x.(x \K.K K (\_.\K'.\v.(k K' v)))
K +        =  \k.\K.\x.(x k K (\_.k))
           =  \k.\K.\x.(x k K (\_.\K'.\v.(k K' v)))
A +        =  \k.\K.\x.K x

Remarques :

V M *      =  \k.\K.(M* (V+ k) K)
           =  \k.(M* (V+ k))
V W *      =  \k.\K.(V+ k K W+)
M V *      =  \k.(M* \K.\m.(m k K V+))
S (\f.M) * =  \k.(M*[f:=\k'.\K'.(k (k' K'))] \K.K)
C (\f.M) * =  \k.(M*[f:=\_.k] \K.K)
K (\f.M) * =  \k.(M*[f:=\_.k] k)
A M *      =  \k.(M* \K.K)

Les fonctions sont a la Fischer : elles attendent d'abord la continuation
puis l'argument.

Les continuations sont a la Fischer : elles attendent d'abord la
metacontinuation puis l'argument.

Donc les fonctions prennent dans l'ordre : une continuation, une
metacontinuation, un argument.

*** CPS traduction simple a la Plotkin ***

X +                  = X
A_T->B_U +           = A+ -> (B+ -> U) -> T
Gamma |- V:A +       = Gamma+ |- V+ : A+
Gamma, T |- M:A, U + = Gamma* |- M* : (A+ -> T) -> U

x +        =  x
\x.M +     =  \x.M*
           =  \x.\k.(M* k)
V *        =  \k.k V+
M N *      =  \k.(M* \m.(N* \n.(m n k)))

<M> *      =  \k.(k (M* \x.x))
S +        =  \x.\k.(x \v.\k'.(k' (k v)) \v.v)
C +        =  \x.\k.(x \v.\k'.(k v) \v.v)
K +        =  \x.\k.(x \v.\k'.(k v) k)
A M *      =  \k.(M* \v.v)

S (\f.M) * =  \k.(M*[f=\v.\k'.k' (k v)] \v.v)
C (\f.M) * =  \k.(M*[f=\v.\k'.(k v)] \v.v)
K (\f.M) * =  \k.(M*[f=\v.\k'.(k v)] k)

Note : L'argument de Abort doit être évalué paresseusement. Si on
définissait A + comme étant \x.\k.x, alors on sauterait directement au
toplevel final au lieu du toplevel localement défini par le reset le
plus proche.

En appliquant de manière sélective la traduction de Plotkin (on ne
traduit les commandes, de type "T", mais pas les fonctions, de type
"A->B"), on obtient la traduction double de Kameyama-Hasegawa.

En appliquant de manière sélective la traduction de Fisher, on obtient
une traduction double intermédiaire entre celle de Danvy-Filinski et
celle de Kameyama-Hasegawa.

On pourrait avoir 4 traductions différentes en théorie, toutes
équivalentes a symétrie près dans la curryfication des arguments.

Note : Si on suppose dans S (\f.M) et C (\f.M) que toutes les
occurrences de f apparaissent dans un contexte de la forme <f N> ou 
S (\f.(k N)) ou C (\f.(k N)), alors on peut simplifier les traductions
en prenant S + = C + = \x.\k.(x k \v.v).

*** CPS traduction double de Kameyama-Hasegawa ***

X +                  = X
A_T->B_U +           = A+ -> (B+ -> ~~U) -> ~~T
Gamma |- V:A +       = Gamma+ |- V+ : A+
Gamma, T |- M:A, U + = Gamma* |- M* : (A+ -> ~~T) -> ~~U

x +        =  x
\x.M +     =  \x.M*
           =  \x.\k.\K.(M* k K)
V *        =  \k.k V+
           =  \k.\K.(k V+ K)
M N *      =  \k.(M* \m.(N* \n.(m n k)))
           =  \k.(M* \m.\K.(N* \n.(m n k) K))

 on pose  J = \x.\K.K x
 et     k^K = \v.(k v K)
 et      k! = \v.\_.(k v)
 et      k# = \v.\k'.\K'.(k v k'^K')

<M> *      =  \k.\K.(M* J (k^K))
S +        =  \x.\k.(x k# J)
C +        =  \x.\k.(x k! J)
           =  \x.\k.\K.(x (\v.\_.\K'.(k v K')) J K)
K +        =  \x.\k.(x k! k)
           =  \x.\k.(x (\v.\_.\K'.(k v K')) k)
A +        =  \x.\k.(J x)
           =  \x.\k.\K.K x

Remarques:

V M *      =  \k.(M* \n.(V+ n k))
V W *      =  \k.(V+ W+ k)
           =  (V+ W+)
M V *      =  \k.(M* \m.(m V+ k))
S (\f.M) * =  \k.(M*[f:=k#] J)         
C (\f.M) * =  \k.(M*[f:=k!] J)         
K (\f.M) * =  \k.(M*[f:=k!] k)
A M *      =  \k.(M* J)

S M *      =  \k.(M* \x.(x k# J))
C M *      =  \k.(M* \x.(x k! J))
K M *      =  \k.(M* \x.(x k! k))

Equations intéressantes :

   k# v J --> k v
   J#     --> J
   J^K    --> K

Les fonctions sont à la Plotkin : elles attendent d'abord l'argument
puis la continuation.

Les continuations sont à la Plotkin : elles attendent d'abord
l'argument puis la métacontinuation.

Les fonctions prennent dans l'ordre : un argument, une continuation et
une métacontinuation.