Le blog de SpiceGuid

Un article de SpiceGuid    Pas de commentaires

À la lecture de The Art of the Propagator je me suis laissé convaincre que l’avenir de la programmation déclarative était dans la propagation logique. L’intérêt de la propagation c’est que le calcul monodirectionnel disparaît, le calcul devient multi-directionnel, la béta-réduction devient la béta-équivalence.

Jusqu’à présent je m’étais toujours dit « et alors, quel intérêt ? ».
C’est là que The Art of the Propagator apporte un argument de poids :

• le calcul monodirectionnel suppose un temps fondamentalement linéaire, il y a un avant et un après la réduction
• le parallélisme c’est quand le temps n’est plus linéaire
• pourquoi chercher à recréer l’illusion du temps linéaire alors qu’il suffit de lever la restriction monodirectionnelle pour adopter le point de vue du parallélisme ?

Ni une ni deux, installation presto de B-Prolog et petite traduction de l’exemple tiré de The Art of the Propagator (le document d’origine utilise des composants logiciels en Scheme à connecter comme pour une simulation de circuit électronique) :

temperature(F,C,K) :-
   C is (F - 32) * 5/9,
   K is C + 273.

J’adore ce style complètement équationnel.

Ce code peut convertir en degrés celsius et degrés en kelvins et même détecter une contradiction entre deux valeurs non convertibles :

| ?- temperature(77,C,K).
C = 25.0
K = 298.0
yes
| ?- temperature(45,C,298).
no

Malheureusement il semblerait que le calcul soit monodirectionnel, tout se passe comme si C était calculé à partir de F puis K à partir de C. Il m’est imposible d’obtenir une réponse sans fournir une valeur pour F :

| ?- temperature(F,25,K).
***  error(instantiation_error,b_EVAL_ARITH_cf/2)
| ?- temperature(F,C,298).
***  error(instantiation_error,b_EVAL_ARITH_cf/2)

Il y a sans doute une façon de le faire en Prolog mais j’aurai aussi vite fait de l’écrire en Caml.

Les circuits sont composés de constantes entières, de variables (réliées à un ou deux composants), d’entrées (limitées à 2), de sorties et d’opérateurs :

type expr =
  | Int of int
  | Var1 of int * expr
  | Var2 of int * expr * expr
  | Input1 of operator
  | Input2 of operator
  | Output of operator 
and operator =
  <input1:evaluator; input2:evaluator; output:evaluator>
  * expr * expr * expr
and evaluator =
  (expr -> int option) -> expr -> expr -> int option 

L’évaluateur eval calcule la valeur d’un point du circuit.
Le paramètre m est un marqueur destiné à éviter les parcours en boucle.
Etant donné l’environnement env, il suffira d’appeler l’évaluateur sur un noeud contenant une variable pour connaître sa valeur.

Cette façon de faire me paraît plus dénotationnelle que la version Scheme de The Art of the Propagator qui donne une sémantique opérationnelle à l’aide d’un scheduler.

Remarquez que du fait que mon circuit est paramétré par un environnement j’obtiens gratuitement un moyen d’abstraction sur les circuits propagateurs. Je n’aurai qu’à créer un nouvel environnement pour changer les 3 températures alors qu’avec la version Scheme il faut explicitement reconnecter un nouveau circuit (les températures sont immutables).

let rec eval env m = function
  | Var1(n,e1) ->
      ( match List.nth env n,eval env m e1 with
      | None,x | x,None -> x
      | Some x,Some y when x = y -> Some x
      | _ -> failwith "incoherence" )
  | Var2(n,e1,e2) ->
      ( match List.nth env n,eval env m e1,eval env m e2 with
      | x,None,None | None,x,None | None,None,x -> x
      | None,Some y,Some z when y = z -> Some z
      | Some x,None,Some z when x = z -> Some x
      | Some x,Some y,None when x = y -> Some y
      | Some x,Some y,Some z when x = y && y = z -> Some z
      | _ -> failwith "incoherence" )
  | Int n ->
      Some n
  | Input1 p ->
      if p == m then None else 
      let op,a,b,c = p in op#input1 (eval env p) b c
  | Input2 p ->
      if p == m then None else 
      let op,a,b,c = p in op#input2 (eval env p) a c
  | Output p ->
      if p == m then None else 
      let op,a,b,c = p in op#output (eval env p) a b

La classe operation nous permettra d’ajouter facilement des opérateurs.

class operation fa fb fc =
  let result f x y =
    match x,y with
    | Some x,Some y -> Some(f x y)
    | _ -> None
  in
  object
    method input1 : evaluator =
      fun eval b c -> result fa (eval c) (eval b)
    method input2 : evaluator = 
      fun eval a c -> result fb (eval c) (eval a)
    method output : evaluator = 
      fun eval a b -> result fc (eval a) (eval b)  
  end

Trois opérateurs élémentaires:

let add = new operation ( - ) ( - ) ( + )
and mul = new operation ( / ) ( / ) ( * ) 
and sub = new operation ( + ) (fun c a -> a - c) ( - ) 

La construction du circuit :

let t =
  let
  rec f = Var1(0,Output add32)
  and c = Var2(1,Input2 mul9,Input2 add273)
  and k = Var1(2,Output add273)
  and add32  = add, Int 32, Input2 mul5, f
  and mul5   = mul, Int 5, Input2 add32, Output mul9
  and mul9   = mul, Int 9, c, Output mul5
  and add273 = add, Int 273, c, k
  in
  object
    method fahrenheit = f
    method celsius = c
    method kelvin = k
  end

L’objet renvoyé en résultat fourni un accès direct aux trois sondes de température du circuit.

Une rédéfinition de eval pour démarrer avec un marqueur fantôche :

let eval env expr =
  let start = add,Int 0,Int 0,Int 0
  in  eval env start expr

Des exemples d’inférence :

# eval [None;Some 25;None]  t#fahrenheit;;
- : int option = Some 77
# eval [Some 77;None;None]  t#celsius;;
- : int option = Some 25
# eval [Some 77;None;None]  t#kelvin;;
- : int option = Some 298
# eval [None;None;Some 298] t#fahrenheit;;
- : int option = Some 77

Cohérence et incohérence de valeurs multiples :

# eval [None;Some 25;Some 298] t#fahrenheit;;
- : int option = Some 77
# eval [None;Some 23;Some 298] t#fahrenheit;;
Exception: Failure "incoherence".

En ajoutant un peu de sucre syntaxique il devrait être possible de déclarer temperature comme en Prolog.

Avec le code de eval on a déjà l’élément de base pour écrire un interpréteur pour un langage déclaratif multi-directionnel.
Cependant on irait pas très loin car The Art of the Propagator ne dit pas comment exploiter la multi-directionnalité sur des exemples plus convaincants. Peut-on par exemple exécuter un dérivateur formel « à l’envers » pour obtenir un intégrateur formel par propagation ?
Si oui, comment ? Si non, pourquoi ?

Au bout du compte la thèse est avare en exemples consistants et se contente de conjecturer de possibles champs d’application, notamment dans les domaines des TMS (Truth aintenance Systems), de la recherche dirigée par les dépendances et la FRP (Functional reactive Programming).