使用延迟模式从固定点算子计算（无限）树 [英] Compute an (infinite) tree from fixpoint operator using delay modality

问题描述

这是一个涉及循环绑定和无限数据结构的函数式编程难题。有一些背景知识，所以请牢牢记住。

设置。让我们定义一个表示递归数据类型的数据类型：

  type Var = String 
 data STerm = SMu Var STerm 
 | SVar Var 
 | SArrow STerm STerm 
 | SBottom 
 | STOP 
派生（显示）
  

即 t :: =μα。 t | α| t→t | ⊥| ⊤。请注意，⊥表示没有居民的类型，而⊤表示所有居民的类型。请注意，（μα。α）=⊥，因为μ是至少定点操作符。

我们可以将递归数据类型解释为无限树，由重复展开μα而产生。 t 到 t [α↦μα。吨] 。 （有关此过程的正式说明，请参见 http://lucacardelli.name/Papers/SRT.pdf）在Haskell中，我们可以定义一种懒惰树，它没有μ-binder或变量：

 数据LTerm = LArrow LTerm LTerm 
 | LBottom 
 | LTop 
导出（显示）
  

，在普通的Haskell中，转换函数从1到其他：

  convL :: [（Var，LTerm）]  - > STerm  - > LTerm 
 convL _ STop = LTop 
 convL _ SBottom = LBottom 
 convL ctx（SArrow t1 t2）= LArrow（convL ctx t1）（convL ctx t2）
 convL ctx（SVar v）
 |只要<<  -  lookup v ctx = l 
 |否则=错误未绑定变量
 convL ctx（SMu vt）= fix（\ r  - > convL（（v，r）：ctx）t）
  

然而，这个函数有一个问题：它不是生产性的。如果你运行 convL []（SMux（SVarx）），你将会无限循环。在这种情况下，我们宁愿得到 LBottom 。一个有趣的练习是直接修复这个功能，使其具有生产力;然而，在这个问题中，我想以不同的方式解决问题。

延迟模式下的生产力当我们如上构建循环数据结构时，我们需要确保在构建它们之前不使用我们的计算结果。延迟模式是确保我们编写高效（非无限循环）程序的一种方式。基本思想很简单：如果类型 Int 意味着我今天有一个整数，则定义一个类型构造函数 D ，所以 D Int 表示我有一个类型为 Int 明天的值。 D 是一个Functor和一个Applicative（但不是一个monad。）

   -  D是抽象的;你不允许模式匹配
 newtype D a = D a 
 deriving（Show）
 
 instance Functor D其中
 fmap f（D a）= D（fa）
 
实例应用D其中
 D f * D a = D（fa）
 pure x = D x 
  

c> D ，我们定义一个定点操作符：它说要构造一个 a 的值，你可以访问 a 您正在构建，只要您明天使用 。

  fixD ::（D a  - > a） - > a 
 fixD f = f（D（fixD f））
  

例如，Stream既包含今天的价值 a ，又包含我必须在明天产生的流流a p>

 数据Stream a = Cons a（D（Stream a））
  

使用 fixD ，我可以定义一个 map 函数由于对 map 的递归调用仅用于生成明天需要的值，所以保证是有效的。

  instance Functor Stream其中
 fmap f = fixD $ \go（Cons x xs） - >缺点（fx）（go * xs）
  

问题。 strong>这是 LTerm 的一个变体，带有明确的延迟模式。

  data Term = Arrow（D Term）（D Term）
 |底部
 |使用 fixD  $（b 
 $ / code> 



（不允许非结构性递归引用），我该如何编写一个函数 conv :: STerm - > Term （或 conv :: STerm - > D Term ）？
特别有趣的测试用例是 SMux（SArrow STop（SMuy（SVarx）））;在结果结构中应该没有Bottoms！





更新。我不小心排除了 STerm code>，这不是问题的意图;我已经重写了删除该限制。

解决方案

你打算只禁止不受限制的递归（在 SMu 大于 convL 的情况下，修复中的结构递归 SArrow case？

我不认为这有一个没有结构递归的解决方案 STerm ，因为那样的话，即使在一个无限的 STerm 中，我们也必须保持高效，比如：

< pre class =lang-hs prettyprint-override> foldr（\\\
- > SMu（x++ show n））undefined [0 ..] - μα。 μβ。 μγ。 μδ。 ...


使用 STerm ，似乎诀窍是在上下文中存储任一术语（D Term）。当我们通过一个 Arrow 并产生一个 D 时，我们可以将所有的 / code> s to Left s

$ b

  type Ctx = [（Var，E Term（D Term））] 
 
 dCtx :: Ctx  - > D ctx 
 dCtx =遍历（遍历（fmap Left。或者纯粹的id））
 
 conv :: STerm  - > Ctx  - >期限
 conv STop _ =最高
 conv SBottom _ =最低
 conv（SArrow t1 t2）ctx =箭头（fmap（conv t1）（dCtx ctx））（fmap（conv t2）（ dCtx ctx））
 conv（SVar v）ctx =案例查找v ctx of 
 Nothing  - >错误未绑定变量
 Just（Left t） - > t 
 Just（Right _） - >底部
 conv（SMu vt）ctx = fixD（\ dr  - > conv t（（v，Right dr）：ctx））
  

Here is a functional programming puzzle involving loop-tying and infinite data structures. There is a bit of background, so hang tight.

The setting. Let us define a data type representing recursive data types:

type Var = String
data STerm = SMu Var STerm
           | SVar Var
           | SArrow STerm STerm
           | SBottom
           | STop
   deriving (Show)

i.e. t ::= μα. t | α | t → t | ⊥ | ⊤. Note that ⊥ denotes the type with no inhabitants, while ⊤ denotes the type with all inhabitants. Note that (μα. α) = ⊥, as μ is a least fixpoint operator.

We can interpret a recursive data type as an infinite tree, arising from repeatedly unfolding μα. t to t[α ↦ μα. t]. (For a formal description of this process, see http://lucacardelli.name/Papers/SRT.pdf) In Haskell, we can define a type of lazy trees, which don't have μ-binders or variables:

data LTerm = LArrow LTerm LTerm
           | LBottom
           | LTop
   deriving (Show)

and, in ordinary Haskell, a conversion function from one to the other:

convL :: [(Var, LTerm)] -> STerm -> LTerm
convL _ STop    = LTop
convL _ SBottom = LBottom
convL ctx (SArrow t1 t2) = LArrow (convL ctx t1) (convL ctx t2)
convL ctx (SVar v)
    | Just l <- lookup v ctx = l
    | otherwise = error "unbound variable"
convL ctx (SMu v t) = fix (\r -> convL ((v, r) : ctx) t)

However, there is a problem with this function: it's not productive. If you run convL [] (SMu "x" (SVar "x")) you will infinite loop. We would rather get LBottom in this case. An interesting exercise is to directly fix this function so that it is productive; however, in this question I want to solve the problem differently.

Productivity with the delay modality. When we build cyclic data structures as above, we need to make sure we do not use the results of our computations before we have constructed them. The delay modality is a way of ensuring that we write productive (non infinite looping) programs. The basic idea is simple: if the type Int means that I have an integer today, I define a type constructor D, so that D Int means that I have a value of type Int tomorrow. D is a Functor and an Applicative (but NOT a monad.)

-- D is abstract; you are not allowed to pattern match on it
newtype D a = D a
   deriving (Show)

instance Functor D where
    fmap f (D a) = D (f a)

instance Applicative D where
    D f <*> D a = D (f a)
    pure x = D x

With D, we define a fixpoint operator: it says that to construct a value of a, you can have access to the a you are constructing, as long as you only use it tomorrow.

fixD :: (D a -> a) -> a
fixD f = f (D (fixD f))

For example, a Stream consists both of a value a I have today, and a stream Stream a which I have to produce tomorrow.

data Stream a = Cons a (D (Stream a))

Using fixD, I can define a map function on streams which is guaranteed to be productive, since the recursive call to map is only used to produced values that are needed tomorrow.

instance Functor Stream where
    fmap f = fixD $ \go (Cons x xs) -> Cons (f x) (go <*> xs)

The problem. Here is a variant of LTerm with an explicit delay modality.

data Term = Arrow (D Term) (D Term)
          | Bottom
          | Top
    deriving (Show)

Using fixD (no non-structurally recursive references allowed), how do I write a function conv :: STerm -> Term (or conv :: STerm -> D Term)? A particularly interesting test case is SMu "x" (SArrow STop (SMu "y" (SVar "x"))); there should be no Bottoms in the resulting structure!

Update. I accidentally ruled out structural recursion on STerm, which was not the intent of the question; I've reworded to remove that restriction.

解决方案

Do you intend to forbid just the unrestricted recursion (fix) in the SMu case of convL, or also the structural recursion in the SArrow case?

I don’t think this has a solution without structural recursion on STerm, because then we would have to be productive even on an infinite STerm such as:

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

To do this with structural recursion on STerm, it seems the trick is to store Either Term (D Term) in the context. When we pass through an Arrow and produce a D, we can convert all the Rights to Lefts.

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))

这篇关于使用延迟模式从固定点算子计算（无限）树的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！