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

----------

Une semantique a petits pas iterative avec des contextes de reduction:

"Reduction semantics" pour les expressions arithmetiques
--------------------------------------------------------


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


Redexes potentiels:

  rp ::= n1 - n2


Regle de reduction:

  n1 - n2 -> n3

(pour les entiers Z, tous les redexes potentiels sont de vrais redexes;
 pour les entiers naturels, pas tous ne le sont:
   n1 - n2 -> n3   si n1 >= n2
 un redex potentiel qui n'en est pas un vrai est "coince" (stuck).)


Fonction de contraction:

  contracte : redex_potentiel -> expression + stuck
  contracte (n1 - n2) = n3   si n3 = n1 - n2

et si on n'a que des entiers naturels,

  contracte (n1 - n2) = n3     si n1 >= n2 et n3 = n1 - n2
  contracte (n1 - n2) = stuck  si n1 < n2


Contextes de reduction:

C  : cont
C ::= [] | [C e] | [v C]


Recomposition: 

             recompose : cont * expression -> expression
     recompose ([], e) = e
recompose ([C e2], e1) = recompose (C, e1 - e2)
recompose ([n1 C], e2) = recompose (C, n1 - e2)


Decomposition:

dec_ou_val = (C, rp) | v

fonction de decomposition:

             decompose_term : expression * cont -> dec_ou_val
      decompose_term (n, C) = decompose_cont (C, n)
decompose_term (e1 - e2, C) = decompose_term (e1, [C e2])

             decompose_cont : cont * valeur -> dec_ou_val
     decompose_cont ([], n) = n
  decompose_cont ([C e], n) = decompose_term (e, [n c])
decompose_term ([n1 C], n2) = (C, n1 - n2)

  decompose : expression -> dec_ou_val
decompose e = decompose_term (e, [])


Un pas de reduction:

reduis : expression -> expression + stuck

si decompose e = v
alors reduis e = stuck

si decompose e = (C, rp)
et contracte rp = stuck
alors reduis e = stuck

si decompose e = (C, rp)
et contracte rp = c
alors reduis e = recompose (C, c)


Evaluation basee sur la reduction iteree:

itere : red_ou_val -> valeur + erreur

itere v = v

si contracte rp = stuck
alors itere (C, rp) = stuck

si contracte rp = c
alors itere (C, rp) = itere (decompose (recompose (C, c)))


Exercice 1:
  Implementer la "reduction semantics" ci-dessus et la tester.


Exercice 2:
  Optimiser l'etape de recomposition / decomposition
  en une fonction "refocus".


Exercice 3:
  Obtenir une machine abstraite.

----------

% fin de danvy-ex2.txt