% danvy-ex1.txt
% exercices pour JFLA 2014
% 8 janvier 2014
% Olivier Danvy <danvy@cs.au.dk>

----------

1. Les expressions arithmétiques
   -----------------------------

Expressions:

n  :  int

e  :  expression
e ::= n | e - e

p  :  programme
p ::= e


Exemples:

p0 = 0
p1 = 10 - 6
p2 = (10 - 6) - (7 - 2)
p3 = (7 - 2) - (10 - 6)
p4 = 10 - (2 - 3)


Valeurs:

v  :  valeur
v ::= n


Valeurs expressibles:

ve  :  valeur_expressible
ve ::= v


Interprétation:

------
n => n

e1 => n1   e2 => n2   n1 - n2 = n3
----------------------------------
      e1 - e2 => n3


On interprète le programme e en la valeur n si le jugement

  e => n

est satisfait.


Exercice 0:
  Programmer l'interprète ci-dessus (disons en OCaml)
  et le tester sur les exemples.

  évalue_0 : expression -> valeur_expressible
  interprète_0 : programme -> valeur_expressible


Exercice 1:
  CPS-transformer (en appel par valeur, de gauche à droite)
  la fonction évalue_0,
  et l'appeler dans la fonction principale de l'interprète
  avec comme continuation initiale la fonction identité.

      évalue_1 : expression -> (valeur_expressible -> 'a) -> 'a
  interprète_1 : programme -> valeur_expressible


Exercice 2:
  Défonctionaliser la continuation de évalue_1.

         cont ::= ...

    continue_2 : cont -> valeur -> valeur
      évalue_2 : expression -> cont -> valeur
  interprète_2 : programme -> valeur

  Le type de données ("data type") cont représente
  la grammaire des contextes.

  Les deux fonctions mutuellement récursives évalue_2
  et continue_2 implémentent une machine abstraite,
  c'est à dire un système de transition d'états.

----------

2. Les expressions arithmétiques, avec des erreurs
   -----------------------------------------------

Expressions:

n  :  nat

e  :  terme
e ::= n | e - e

p  :  programme
p ::= e


Exemples:

p0 = 0
p1 = 10 - 6
p2 = (10 - 6) - (7 - 2)
p3 = (7 - 2) - (10 - 6)
p4 = 10 - (2 - 3)


Valeurs:

v  :  valeur
v ::= n


Erreurs:

s  :  erreur


Valeurs expressibles:

ve  :  valeur_expressible
ve ::= v | s


Interprétation:

------
n => n

     e1 => s
------------
e1 - e2 => s

e1 => n1   e2 => s
------------------
      e1 - e2 => s

e1 => n1   e2 => n2   n1 < n2
-----------------------------
      e1 - e2 => "underflow"

e1 => n1   e2 => n2   n1 >= n2   n1 - n2 = n3
---------------------------------------------
      e1 - e2 => n3

On interprète le programme e en la valeur n si le jugement

  e => n

est satisfait, et en l'erreur s si le jugement

  e => s

est satisfait.


Exercice 0:
  Programmer l'interprète ci-dessus
  et le tester sur les exemples.

  évalue_0 : terme -> valeur_expressible
  interprète_0 : programme -> valeur_expressible


Exercice 1:
  CPS-transformer (en appel par valeur, de gauche à droite)
  la fonction évalue_0,
  et l'appeler dans la fonction principale de l'interprète
  avec comme continuation initiale la fonction identité.

      évalue_1 : terme -> (valeur_expressible -> 'a) -> 'a
  interprète_1 : programme -> valeur_expressible


Exercice 2:
  Diviser la continuation
    valeur_expressible -> 'a
  en deux:
    (valeur -> 'a) * (erreur -> 'a)
  et adapter évalue_1 et interprète_1.

      évalue_2 : terme -> (valeur -> 'a) -> (erreur -> 'a) -> 'a
  interprète_2 : programme -> valeur_expressible


Exercice 3:
  Spécialiser le co-domaine des continuations et de la fonction
  d'évaluation pour qu'il ne soit plus polymorphique
  mais qu'il soit valeur_expressible, et
  court-circuiter la seconde continuation pour ne pas continuer
  en cas d'erreur.

      évalue_3 : terme -> (valeur -> valeur_expressible) -> valeur_expressible
  interprète_3 : programme -> valeur_expressible

  (NB. Maintenant il n'y a plus qu'une continuation et elle n'est
  appliquée que s'il n'y a pas eu d'erreur.)

Exercice 4:
  Défonctionaliser la continuation de évalue_3.

         cont ::= ...

    continue_4 : cont -> valeur -> valeur_expressible
      évalue_4 : terme -> cont -> valeur_expressible
  interprète_4 : programme -> valeur_expressible

  Le type de données ("data type") cont représente
  la grammaire des contextes.  (NB. A-t-il changé
  par rapport à l'exercice précédent?)

  Les deux fonctions mutuellement récursives évalue_4
  et continue_4 implémentent une machine abstraite,
  c'est à dire un système de transition d'états,
  qui s'arrête soit tout de suite en cas d'erreur,
  soit à la fin du calcul.

----------

Le lambda-calcul
----------------

Termes:

n : int

x : identificateur

t  : terme
t ::= x | \x.t | t t

p  :  programme
p ::= t
      où t est fermé (i.e., sans variables libres)


Exemples:

p0 = (\x.x)
p1 = (\x.x) (\x.x)
p2 = (\x.\f.f x) (\y.y) (\x.x)


Valeurs et environnements:

e  :  environnement
v ::= nil | (identificateur, valeur) :: environnement

v  :  valeur
v ::= (\x.t, e)


Opérateur algébrique:

lookup : identificateur -> environnement -> valeur


Contextes d'évaluation:

C ::= [] | [C (t, e)] | [v C]


Machine abstraite (dite "CEK"):

    <x, e, C>_eval -> <C, v>_cont
                      où v = lookup x e
 <\x.t, e, C>_eval -> <C, (\x.t, e)>_cont
<t0 t1, e, C>_eval -> <t0, e, [C (t1, e)]>

           <[], v>_cont -> v
   <[C (t, e)], v>_cont -> <t, e, [v C]>_eval
<[(\x.t, e) C], v>_cont -> <t, (x, v) :: e, C>_eval


Exercice 0:
  Programmer cette machine abstraite.


Exercice 1:
  Cette machine abstraite est en forme défonctionalisée.
  La refonctionaliser.


Exercice 2:
  Le résultat de l'Exercice 1 est en CPS.
  L'exprimer en style direct.


Exercice 3:
  Le résultat de l'Exercice 2 est en forme défonctionalisée
  (dans le sens que les fermetures sont en forme défonctionalisée
  triviale).
  Le refonctionaliser, et caractériser le résultat.

----------

% fin de danvy-ex1.txt