Bonjour,
J'aimerais juste faire une rapide "sanity check" sur les indices de De Bruijn
* * r_index * / * [4] Nat = [..] * [3] a = [..] r_index r_offset * [2] b = [..] \ / * [1] zero = Nat [..] || Nat DBI = 4 - 1 = 3 (zero, a, b) * [0] one = Nat [..] || Nat DBI = 4 - 0 = 4 * || Zero DBI = 1
Dans le cas d'une récursion j'ai besoin de repérer les variables libres pour les push dans le contexte de la lambda. Cette étape va être faite deux fois, une fois pendant le lexp parsing pour déterminer l'index et une fois pendant l'évaluation pour créer le contexte de la lambda.
Afficher les réponses par date
r_index/- [4] Nat = [..]
- [3] a = [..] r_index r_offset
- [2] b = [..] \ /
- [1] zero = Nat [..] || Nat DBI = 4 - 1 = 3 (zero, a, b)
- [0] one = Nat [..] || Nat DBI = 4 - 0 = 4
|| Zero DBI = 1
Dans le cas d'une récursion j'ai besoin de repérer les variables libres pour les push dans le contexte de la lambda.
Non. Si tu as
a : <type1> b : <type2> c : <type3> a = <exp1> b = <exp2> c = <exp3>
alors a, b, et c sont tous les trois placés dans le même `let` et <exp1>, <exp2>, et <exp3> utilisent le même environnement (celui qui contient a, b, et c (plus tout ce qui vient avant)).
Cela est vrai indépendemment des variables libres de a, b, et c.
Cette étape va être faite deux fois, une fois pendant le lexp parsing pour déterminer l'index et une fois pendant l'évaluation pour créer le contexte de la lambda.
Non, pour l'évaluateur, un let récursif comme notre `Let` s'interprète généralement de la manière suivante:
newenv = append ([ERROR, ERROR, ERROR], oldenv) (nth 0 newenv) := eval exp1 newenv (nth 1 newenv) := eval exp2 newenv (nth 2 newenv) := eval exp3 newenv
Stefan
Je pensais plus à quelque chose comme cela:
Nat = inductive_ (dNat) (zero) (succ Nat);
zero = inductive-cons Nat zero; succ = inductive-cons Nat succ;
one = (succ zero); two = (succ one); three = (succ three);
tonum = lambda x -> case x % | (succ y) => (1 + (tonum y)) % ENV: [tonum[2]; x[1]; y[0]] | _ => 0;
tonum marche pour seulement une récursion parce que pour le second appel à tonum l'index de tonum n'est plus 2 mais 4 (2 x et 2 y). La solution que j'avais pensé était de push le body de tonum à l'appel de la fonction ainsi la distance du body de tonum est toujours de 2. (Cela revient à traiter tonum comme une fonction avec un argument implicite qui est lui même) Sinon il faut calculer pendant l'évaluation l'offset de tonum ce qui serait certainement plus efficace.
tonum = lambda x -> case x % | (succ y) => (1 + (tonum y)) % ENV: [tonum[2]; x[1]; y[0]] | _ => 0;
tonum marche pour seulement une récursion parce que pour le second appel à tonum l'index de tonum n'est plus 2 mais 4 (2 x et 2 y).
Non. Lors de l'appel récursif, tu reprends l'environnement de tonum (i.e. où il n'y avait pas encore de x ni de y) et tu y ajoutes un nouveau x et ensuite un nouveau y.
Ça fait partie de la différence entre lexical-scoping et dynamic-scoping.
Stefan
-
Pierre Delaunay -
Stefan Monnier -
Stefan Monnier