haskell - 遅延モダリティを使用して固定点演算子から (無限) ツリーを計算します

Answer 1

の場合は無制限再帰 ( fix)だけを禁止するつもりですか、それとも構造的再帰も禁止するつもりですか?SMuconvLSArrow

での構造的再帰なしでは、これには解決策がないと思います。次のようなSTerm無限でも生産的でなければならないからです。STerm

foldr (\n -> SMu ("x" ++ show n)) undefined [0..]  -- μα. μβ. μγ. μδ. …

の構造的再帰でこれを行うには、コンテキストSTermに格納するのがコツのようです。Either Term (D Term)an を通過しArrowて a を生成すると、すべてのs をs にD変換できます。RightLeft

type Ctx = [(Var, Either Term (D Term))]

dCtx :: Ctx -> D Ctx
dCtx = traverse (traverse (fmap Left . either pure id))

conv :: STerm -> Ctx -> Term
conv STop _ = Top
conv SBottom _ = Bottom
conv (SArrow t1 t2) ctx = Arrow (fmap (conv t1) (dCtx ctx)) (fmap (conv t2) (dCtx ctx))
conv (SVar v) ctx = case lookup v ctx of
                      Nothing -> error "unbound variable"
                      Just (Left t) -> t
                      Just (Right _) -> Bottom
conv (SMu v t) ctx = fixD (\dr -> conv t ((v, Right dr) : ctx))

Answer 2

私の直感では、コンテキストには遅延語のみを含める必要があります。そうすれば、元の のconv ctx (SMu "x" t)ように と同等になります。fixD (\d -> conv ((x,r):ctx) t)convL

この場合、遅延項を単に矢印で許可するのではなく、データ構造に含める一般的な方法が必要です。

data Term = Arrow Term Term
          | Bottom
          | Top
          | Next (D Term)

最初の試みでconvは、次のようになります。

conv :: [(Var, D Term)] -> STerm -> Term
conv _ STop = Top
conv _ SBottom = SBottom
conv ctx (SArrow t1 t2) = Arrow (conv ctx t1) (conv ctx t2)
conv ctx (SVar v)
  | Just l <- lookup v ctx = Next l
  | otherwise = error "unbound variable"
conv ctx (SMu v t) = fixD (\r -> conv ((x,r):ctx) t)

ただし、これは への無防備な再帰呼び出しを使用しconvます。それを避けたい場合は、すべてのfixD再帰呼び出しをNext.

conv :: [(Var, D Term)] -> STerm -> Term
conv = fixD step where
        step _ _ STop = Top
        step _ _ SBottom = Bottom
        step d ctx (SArrow t1 t2) = Arrow (Next $ d <*> pure ctx <*> pure t1) 
                                          (Next $ d <*> pure ctx <*> pure t2)
        step d ctx (SVar v)
          | Just l <- lookup v ctx = Next l
          | otherwise = error "unbound variable"
        step d ctx (SMu v t) = fixD (\r -> 
                                    Next $ d <*> pure ((x,r):ctx) <*> pure t)

conv [] SMu "x" (SArrow SBottom (SMu "y" (SVar "x")))結果の構造にはまだ底があるため、これがまさにあなたが探しているものかどうかはわかりません。出したいタイプは？