你如何从lambda术语转化为交互网络？ [英] How do you translate from lambda terms to interaction nets?

问题描述

在本文中，作者建议翻译在lambda术语之间：

On this paper, the author suggests a translation between lambda terms:

data Term = Zero | Succ Term | App Term Term | Lam Term

和互动网络：

and interaction nets:

data Net = -- if I understood correctly
    Apply Net Net Net 
    | Abstract Net Net Net
    | Delete Net Net Int
    | Duplicate Net Net Net Int
    | Erase Net

不幸的是我无法理解他的编译算法。看起来像是实际的算法丢失了，我不知道他在第三页上的图像意味着什么。我试着通过查看已发布的源代码来了解它，但作者使用他自己的图形重写DSL来定义它，所以我必须先学习它。作为一个普通的Haskell函数实现翻译的准确程度如何？

Unfortunately I can not understand his compilation algorithm. It seems like the actual algorithm is missing, and I have no idea what he means with the images on the third page. I've tried understanding it by looking at the published source code, but the author defines it using his own graph rewriting DSL so I would have to learn it first. How exactly is the translation implemented as a normal Haskell function?

推荐答案

我有一个使用 STRef s以可变方式表示网络图结构：



I have an implementation of interaction net reduction in Haskell that uses STRefs to represent the net graph structure in a mutable way:

data NodeType = NRot
              | NLam
              | NApp
              | NDup Int
              | NEra
             deriving (Show)

type NodeID = Int
type Port s = STRef s (Node s, PortNum)

data Node s = Node
    { nodeType :: !NodeType
    , nodeID :: !NodeID
    , nodePort0, nodePort1, nodePort2 :: !(Port s)
    }

从lambda项转换是在单独模块。这不是我写过的最好的代码，因为它是 Javascript实现的直译，和我没有真正花时间了解JS版本在做什么：

Conversion from lambda terms is implemented in a separate module. It is not the nicest code I've ever written, because it's a straight transliteration of a Javascript implementation and I didn't really take the time to understand what the JS version is doing:

encodeLam :: Lam -> IntNet s (Node s)
encodeLam lam = do
    nextTag <- do
        ref <- lift $ newSTRef 0
        return $ lift $ do
            modifySTRef ref succ
            readSTRef ref

    let go scope up (Lam body) = do
            del <- mkNode NEra
            lam <- mkNode NLam
            linkHalf lam P0 up
            link (lam, P1) (del, P0)
            link (del, P1) (del, P2)
            bod <- go (lam:scope) (lam, P2) body
            linkHalf lam P2 bod
            return (lam, P0)
        go scope up (App f e) = do
            app <- mkNode NApp
            linkHalf app P2 up
            linkHalf app P0 =<< go scope (app, P0) f
            linkHalf app P1 =<< go scope (app, P1) e
            return (app, P2)
        go scope up (Var v) = do
            let lam = scope !! v
            (target, targetPort) <- readPort lam P1
            case nodeType target of
                NEra -> do
                    linkHalf lam P1 up
                    return (lam, P1)
                _ -> do
                    dup <- mkNode . NDup =<< nextTag
                    linkHalf dup P0 (lam, P1)
                    linkHalf dup P1 up
                    link (dup, P2) =<< readPort lam P1
                    linkHalf lam P1 (dup, P0)
                    return (dup, P1)

    root <- asks root
    enc <- go [] (root, P0) lam
    linkHalf root P0 enc
    return root

它还实现了相反的转换：

It also implements the reverse transformation:

decodeLam :: Node s -> IntNet s Lam
decodeLam root = do
    (setDepth, getDepth) <- do
        ref <- lift $ newSTRef mempty
        let set node depth = lift $ modifySTRef ref $
                             IntMap.insertWith (\ _new old -> old) (nodeID node) depth
            get node = lift $ (! nodeID node) <$> readSTRef ref
        return (set, get)

    let go depth exit (node, port) = do
            setDepth node depth
            case nodeType node of
                NDup _ -> do
                    let (port', exit') = case port of
                            P0 -> (head exit, tail exit)
                            _ -> (P0, port:exit)
                    go depth exit' =<< readPort node port'
                NLam -> case port of
                    P1 -> do
                        depth' <- getDepth node
                        return $ Var (depth - depth' - 1)
                    _ -> Lam <$> (go (succ depth) exit =<< readPort node P2)
                NApp -> do
                    f <- go depth exit =<< readPort node P0
                    e <- go depth exit =<< readPort node P1
                    return $ App f e
    go 0 [] =<< readPort root P0

这篇关于你如何从lambda术语转化为交互网络？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！