Ceci est une variante de "Compute an (infinite) tree from fixpoint operator using delay modality".Calcul de l'arborescence infinie à partir de chemins enracinés à l'aide de la modalité de délai
Le paramètre. Nous étudions un langage d'arbres binaires, augmentée avec la possibilité de se référer à d'autres nœuds arbitraires dans l'arbre par un chemin de la racine:
type Path = [Bool]
data STree = SNode STree STree
| SPath Path
| SLeaf Int
deriving (Show)
Un chemin est défini dans le contexte d'une racine, et identifie les sous-arbre trouvé en suivant successivement les enfants gauche/droit quand nous voyons False/True dans le chemin. Par exemple, le chemin [False, True] identifie SLeaf 2 dans l'arborescence SNode (SNode (SLeaf 1) (SLeaf 2)) (SLeaf 3).
Ces arbres peuvent être utilisés, par exemple, pour identifier les graphes de flux arbitraires (y compris les graphiques, irréductibles quelque chose qui est impossible avec les opérateurs de point fixe.)
On peut considérer l'arbre infini induit par cette description.
data Tree = Node Tree Tree
| Leaf Int
deriving (Show)
est ici une fonction de conversion de l'un à l'autre, en utilisant une fonction auxiliaire follow qui trouve la sous-arborescence à un chemin d'un arbre:
follow :: Path -> Tree -> Tree
follow [] s = s
follow (False : p) (Node s _) = follow p s
follow (True : p) (Node _ s) = follow p s
follow _ (Leaf _) = error "bad path"
flatten' :: Tree -> STree -> Tree
flatten' root (SPath p) = follow p root
flatten' root (SNode s1 s2) =
Node (flatten' root s1) (flatten' root s2)
flatten' _ (SLeaf i) = Leaf i
flatten :: STree -> Tree
flatten s = fix (\root -> flatten' root s)
Malheureusement, cette fonction n'est pas productive: elle boucles infinies sur flatten (SPath []).
Le problème. Nous considérons maintenant une variante de cette structure augmentée de la modalité de délai (comme décrit dans "Compute an (infinite) tree from fixpoint operator using delay modality"), ainsi qu'un constructeur Loop pour indiquer les boucles auto-référentielles.
data Tree = Node (D Tree) (D Tree)
| Leaf Int
| Loop
deriving (Show)
Sans l'aide d'appels de fonction non structurellement récursifs (donc, vous pouvez structurellement récursion sur STree et Path), écrire une fonction STree -> Tree (ou similaire) qui se déploie l'arbre infini.
Postscript. Dans de nombreux cas, nous ne voulons pas calculer un déroulement infini: nous voulons le dépliage fini s'il existe, et une erreur sinon. Plus précisément, étant donné le type de données d'origine:
data Tree = Node Tree Tree
| Leaf Int
deriving (Show)
Sans l'aide non structurellement récursive, on peut vouloir écrire une fonction STree -> Maybe Tree (ou similaire) qui se déroule la syntaxe dans un arbre fini si elle existe, et ne le contraire. L'absence d'une modalité de délai dans cette structure garantit qu'elle est finie.
Comme il n'y a aucune instance de la modalité de délai dans cette structure, il semble impossible de le faire avec fixD: nous obtiendrons un résultat retardé que nous ne pourrons jamais utiliser. Il semblerait que nous devions convertir l'arbre en graphe, le trier topologiquement, puis implémenter directement l'algorithme ala élimination gaussienne sans utiliser fixD. Y at-il une autre discipline de typage qui nous permet d'implémenter les dépliages aussi élégamment que dans le code original (faux)? Si c'est le cas, vous pouvez simplement (re) découvrir un autre algorithme pour trouver des cycles dans les graphiques.
Il n'y a rien qu'il peut faire mais une boucle infinie (ou retourner une autre valeur de fond) sur 'flatten (SPath [])'. Il n'existe pas de 'Tree' qui pourrait correspondre à cela. Dans votre second exemple, il pourrait s'agir de 'Loop' mais cela nécessite une détection de boucle. Vous devez être capable de représenter explicitement des références dans l'arbre (qui aurait un constructeur connu) ou de savoir quel constructeur un chemin ira à priori. – Cirdec
Eh bien, il n'est pas trop difficile d'écrire une fonction de terminaison qui utilise 'Loop', mais comme vous le dites, cela nécessite une détection de boucle. La productivité de cette fonction peut-elle être manifestement évidente? C'est la question! (Je ferai aussi remarquer que dans le cas précédent, il y avait un moyen facile de détecter les boucles, moins évident ici!) –