原始递归函数的指称语义表示

Question

有没有办法在Haskell中表示原始递归函数(PRF)的指称语义？

Answer 1

有点.我们可以使用Haskell类或GADT对原始递归函数进行编码.然后我们可以认为原始递归函数是数据类型的等价类.最简单的等价是关于PRF解释的Haskell外延语义.由于Haskell的指称语义,这种表示最终将是不精确的,但让我们探讨一下我们能够获得的接近程度.

原始递归函数

我们将使用维基百科的原始递归函数的定义.A PRF a是具有arity a的原始递归函数,其中a是自然数.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

data PRF (a :: Nat) where
    Const ::                             PRF 'Z
    Succ  ::                             PRF ('S 'Z)
    Proj  :: BNat n                   -> PRF n
    Comp  :: PRF k  -> List k (PRF m) -> PRF m
    PRec  :: PRF k  -> PRF (S (S k))  -> PRF (S k)

Const构造常量返回0的常量函数或arity零Succ是arity one的后继函数.Proj构造投影函数族,每个投影函数在跳过提供的参数数量后都会选出一个参数.Comp使用提供其参数的其他函数列表组成函数.PRec构建一个模式匹配第一个参数的函数.PRec如果第一个参数为零,则将第一个函数应用于其余参数.如果第一个参数不为零,它将第一个参数的前一个作为第一个参数递归到自身,并返回应用于第一个参数的前一个的第二个函数的结果,递归的结果,以及其余的参数.从编译器PRF到Haskell函数的定义中更容易看到这一点.

compile :: PRF n -> List n Nat -> Nat
compile Const = const Z
compile Succ  = \(Cons n Nil) -> S n
compile (Proj n) = go n
    where
        go :: BNat n -> List n a -> a
        go BZero     (Cons h _) = h
        go (BSucc n) (Cons _ t) = go n t
compile (Comp f gs) = \ns -> f' . fmap ($ ns) $ gs'
    where
        gs' = fmap compile gs
        f'  = compile f
compile (PRec f g) = h
    where
        h (Cons Z t)     = f' t
        h (Cons (S n) t) = g' (Cons n (Cons (h (Cons n t)) t))
        f' = compile f
        g' = compile g

以上要求自然数的定义,Nat由类型级自然数限定的自然数BNat,以及具有类型级已知长度的列表List.

import qualified Data.Foldable as Foldable
import System.IO

data Nat = Z | S Nat
    deriving (Eq, Show, Read, Ord)

data List (n :: Nat) a where
    Nil   ::                  List 'Z     a
    Cons  :: a -> List n a -> List ('S n) a

instance Functor (List n) where
    fmap f Nil        = Nil
    fmap f (Cons h t) = Cons (f h) (fmap f t)    

-- A natural number in the range [0, n-1]
data BNat (n :: Nat)  where
    BZero ::           BNat ('S n)
    BSucc :: BNat n -> BNat ('S n)

我们现在有能力编写我们的第一个原始递归函数.我们将写两个身份和添加的例子.

ident :: PRF (S Z)
ident = Proj BZero

add :: PRF (S (S Z))
add = PRec ident (Comp Succ (Cons (Proj (BSucc BZero)) Nil))

请注意,我们在Haskell中重用了声明来简化这些函数的编写; 我们ident在定义中重复使用add.最终,使用Haskell声明的能力将允许我们创建无限或非完整的递归结构,我们可以潜入该PRF类型.

我们可以编写一些示例代码来试用我们的add函数.我们对评估顺序有点偏执seq,hFlush因此我们可以看到我们的表示在以后有多么错误.

mseq :: Monad m => a -> m a
mseq a = a `seq` return a

runPRF :: PRF n -> List n Nat -> IO ()
runPRF f i = 
    do
        putStrLn "Compiling function"
        hFlush stdout
        f' <- mseq $ compile f
        putStrLn "Running function"
        hFlush stdout
        n <- mseq $ f' i
        print n

如果我们运行一个例子,add我们得到一个很好的,令人满意的输出

runPRF add (Cons (S (S Z)) (Cons (S (S (S Z))) Nil))

Compiling function
Running function
S (S (S (S (S Z))))

Haskell声明

我们可以使用Haskell声明做一些有趣且最终具有破坏性的事情.首先,我们将使模式匹配更容易.能够在PRec不提供使用递归结果的函数的情况下使用模式匹配是很好的.match将为我们添加额外的虚拟参数.

match :: (Depths List k) => PRF k -> PRF (S k) -> PRF (S k)
match fz fs = PRec fz (addArgument (BSucc BZero) fs)

要做到这一点,它需要一个辅助函数,它添加参数,addArgument以及一些其他实用程序来测量具有已知类型的列表的大小Depths,比较和转换BNats,并证明递增的自然数仍然在新的约束下.

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}

class Depths f (n :: Nat) where
    depths :: f n (BNat n)

instance Depths List 'Z where
    depths = Nil

instance (Depths List n) => Depths List ('S n) where
    depths = Cons BZero (fmap BSucc depths)

deriving instance Eq (BNat n)
deriving instance Show (BNat n)
deriving instance Ord (BNat n)

bid :: BNat n -> BNat (S n)
bid BZero = BZero
bid (BSucc x) = BSucc (bid x)

addArgument :: (Depths List k) => BNat (S k) -> PRF k -> PRF (S k)
addArgument n f = Comp f . fmap p $ depths
    where
        p d =
            if d' >= n
            then Proj (BSucc d)
            else Proj d'
            where d' = bid d

在写完全合理的东西时,这非常有用

nonZero :: PRF (S Z)
nonZero = match Const (Comp Succ (Cons (Comp Const Nil) Nil))

isZero :: PRF (S Z)
isZero = match (Comp Succ (Cons Const Nil)) (Comp Const Nil)

isOdd :: PRF (S Z)
isOdd = PRec Const (addArgument BZero isZero)

递归Haskell声明

我们也可以编写非常具有破坏性的东西undefined.首先,我们将while使用递归定义构造.我们知道构建的东西while不应该存在于原始递归函数的闭包中.

while :: (Depths List k) => PRF (S k) -> PRF (S k) -> PRF (S k)
while test step = goTest
    where
        --goTest :: PRF (S k)
        goTest  = Comp goMatch (Cons test (fmap Proj depths))
        --goMatch :: PRF (S (S k))
        goMatch = match (Proj BZero) (addArgument BZero goStep)
        --goStep :: PRF (S k)
        goStep  = Comp goTest (Cons step (fmap (Proj . BSucc) depths))

这使我们可以编写一个仅对某些输入不终止的循环.

infiniteLoop :: PRF (S Z)
infiniteLoop = while isOdd (Comp Succ (Cons Succ Nil))

如果我们为偶数运行,比如Z或S (S Z),它会终止返回输入.如果我们以奇数运行它,它永远不会完成.

runPRF infiniteLoop (Cons (S Z) Nil)
Compiling function
Running function

因为我们对它很谨慎,seq并且hFlush我们可以确定编译的值是以星期正常形式存在的,这不是原始的递归函数并且不是简单的undefined.这是因为compile步骤不严格,并且减少到周头正常形式并没有导致一直到正常形式的减少.我们可以通过添加seqs来解决这个问题compile.我只改变了需要它的两种模式.

compile (Comp f gs) = f' `seq` gs' `seq` go
    where
        go = \ns -> f' . fmap ($ ns) $ gs'
        gs' = fmap compile gs
        f'  = compile f
compile (PRec f g) = f' `seq` g' `seq` h
    where
        h (Cons Z t)     = f' t
        h (Cons (S n) t) = g' (Cons n (Cons (h (Cons n t)) t))
        f' = compile f
        g' = compile g

这基本上会PRF在编译时检查它是否有限.

runPRF infiniteLoop (Cons Z Nil)
Compiling function
GHC stack-space overflow: current limit is 33632 bytes.
Use the `-K<size>' option to increase it.

整理

我们谈到的所有类型都没有真正代表一对一的原始递归函数.PRF a除了上面定义的递归结构之外,还有其他东西居住undefined.它也存在于相同原始递归函数的多个表示中.例如,标识函数具有其他定义,包括具有后继函数的前趋函数(我没有定义)的组成.编译的结果List n Nat -> Nat是由具有相同类型的任何Haskell函数居住,其中还包括所有部分递归函数.

为了隐藏同一函数的多个表示,我们可以使用与Haskell相同的技巧:隐藏函数的内部.如果有人可以检查a的唯一方法PRF是严格编译它并将其应用于某些东西,那么没有人可以区分不同表示的相同原始递归函数.

将我们的GADT转换为类型类并仅导出类,并且compile足以隐藏构造函数.

另一个接口,如果我们扭曲我们的头张望了一下,并注意对原始递归函数的公理是像出口可以发现Category规律,Arrow没有arr(其实它的对面arr),和循环的有限形式,仅适用于自然数.

这应该足以让你相信这几乎是可能的.无论我们做什么,我们仍然会被一个额外的居民所困扰undefined.关于如何使其变得更好的进一步讨论属于一个不同的问题,其中包括对它应该如何好的具体问题.