4
4

2 回答 2

6

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))
于 2016-06-16T01:06:10.210 回答
3

My intuition is that the context should contain only delayed terms. That way, conv ctx (SMu "x" t) will be equivalent to fixD (\d -> conv ((x,r):ctx) t), as in the original convL.

If this is the case, then you need a general way to include delayed terms in your data structure, instead of just allowing them in arrows:

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

A first attempt at conv gives us:

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)

However, this uses unguarded recursive calls to conv. If you want to avoid that, you can wrap all the fixD recursive calls in a 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)

I'm not sure if this is exactly what you are looking for, because conv [] SMu "x" (SArrow SBottom (SMu "y" (SVar "x"))) does still have bottoms in the resulting structure. What is the type you want to get out?

于 2016-06-15T23:35:33.533 回答