Salut Vincent,
Voici une première ébauche de la description du problème&solution dont je t'ai parlé, je commence avec une récapitulation pour les gens du "Cc":
Avec les index de deBruijn, on a le problème que lorsqu'on fait un "lookup", tel que typiquement dans `lctx_lookup_type`, on doit faire:
mkSusp t (S.shift (i + 1))
Quand on a de la chance et que le type en question est fermé, ce shift va traverser `t` récursivement (et lazily) pour finalement ne rien faire. C'est pas idéal, mais c'est pas le plus grave.
Le plus grave, c'est quand ce type n'est pas complètement fermé (ce qui est le cas courant, après tout, il suffit qu'il y a une référence à un autre type prédéfini comme `Type`, `Int`, `Bool`, `List, `TypeLevel`, ...), on va non seulement traverser `t` mais le résultat sera différent selon la taille actuelle du `lctx`, donc on se retrouve avec un type comme `List` représenté de manière (légèrement) différente à chaque profondeur, donc notre hash-consing ne peut pas les mettre ensemble.
Dans un système comme Coq, ils évitent en partie ce problème parce que `List` n'est pas dans l'environnement `lctx` mais dans un environnement global.
L'idée pour résoudre ce problème de performance et d'utiliser un mélange de deBruijn index et deBruijn level. En gros l'idée serait la suivante. On aurait nos termes représentés comme suit:
type Term | Lambda Term | App Term Term | LVar Nat | IVar Nat | LocallyIndexed Term
Où le `Var` a été dupliqué en un cas `IVar i` si c'est un index et `LVar l` si c'est un level (lorsque l'environnement a une longueur de N, `LVar i` ≃ `IVar (N - i)`), et on a un nouveau nœud `LocallyIndexed e` qui signifie que toutes les variables libres de `e` sont des `LVar` et toutes les variables non-libres de `e` sont des `IVar`.
Comme ça, maintenant, quand on ajoute `x : τ` dans le `lctx` on peut en fait y mettre `x : LocallyIndexed τ'` de sorte que dans le `lctx_lookup_type` on a plus besoin du shift parce qu'un shift de `LocallyIndexed e` renvoie simplement `LocallyIndexed e`.
Mais il faut maintenant réviser nos substitutions explicites. E.g. on aura probablement besoin d'une substitution pour "fermer":
LocallyIndexed τ[σf] ≃ τ
une autre pour ouvrir:
LocallyIndexed τ ≃ τ[σo]
et des règles pour les composer (et bien sûr une/des règles pour éliminer les shifts quand ils arrivent sur un `LocallyIndexed`).
Stefan
Afficher les réponses par date