表示原始递归函数的指称语义 [英] Representation of denotational semantics of primitive recursive functions

问题描述

有没有一种方法来表示Haskell中原始递归函数（PRF）的指称语义？

。我们可以用Haskell类或GADT编码原始递归函数。然后我们可以认为原始递归函数是数据类型的等价类。最简单的等价是超过了PRF解释的Haskell指称语义。由于Haskell的指称语义，这种表示最终会变得不准确，但让我们探讨一下我们可以接近多少。

原始递归函数

我们将使用维基百科原始递归函数的定义 。 PRF a 是一个原始递归函数，其中a是自然数。

  { - ＃LANGUAGE DataKinds＃ - } 
 { - ＃LANGUAGE KindSignatures＃ - } 
 { - ＃LANGUAGE GADTs＃ - } 
 
数据PRF :: Nat）其中
 Const :: PRF'Z 
 Succ :: PRF（'S'Z）
 Proj :: BNat n  - > PRF n 
 Comp :: PRF k  - >列表k（PRF m） - > PRF m 
 PRec :: PRF k  - > PRF（S（S k）） - > PRF（S k）
  

Const 构造常数函数或零值总是返回0. Succ 是arity one的后继函数。 Proj 构造了一系列投影函数，它们在跳过所提供的参数数量后选出其中一个参数。 Comp 用提供参数的其他函数列表组成一个函数。 PRec 构建一个模式与第一个参数匹配的函数。 PRec 如果第一个参数为零，则将第一个函数应用于其余参数。如果第一个参数不为零，则它以第一个参数的前导作为第一个参数递归到自身中，并返回应用于第一个参数的前导的第二个函数的结果，递归的结果和其余参数。从 PRF 到Haskell函数的编译器定义中，这很容易看出来。

  compile :: PRF n  - >列表n纳特 - > Nat 
 compile Const = const Z 
 compile Succ = \（Cons n Nil） - > S n 
 compile（Proj n）= go n 
 where 
 go :: BNat n  - >列表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'
其中
 gs'= fmap编译gs 
 f'=编译f 
编译（PRec fg）= h 
其中
h（Cons Z t）= f't 
h（Cons（S n）t）= g'（Cons n（Cons（h（Cons nt））t））
 f'=编译f 
 g'=编译g 
  

以上要求定义自然数 Nat ，一个由类型级自然数限制的自然数， BNat ，以及一个类型级已知长度的列表， List 。

 将限定的Data.Foldable导入为可折叠
 import System.IO 
 
 data Nat = Z | S Nat 
导出（Eq，Show，Read，Ord）
 
数据列表（n :: Nat）a其中
 Nil :: List'Z a 
缺点:: a  - >列表n a  - > List（'s n）a 
 
实例Functor（List n）其中
 fmap f Nil =无
 fmap f（Cons ht）= Cons（fh）（fmap ft） 
 
  - 范围[0，n-1]中的自然数
数据BNat（n :: Nat）其中
 BZero :: BNat（'s n）
 BSucc :: BNat n  - > BNat（'s n）
  

我们现在可以编写我们的第一个原始递归函数。我们将为身份和添加写两个例子。

  ident :: PRF（SZ）
 ident = Proj BZero 
 
 add :: PRF（S（SZ））
 add = PRec ident（Comp Succ（Cons（Proj（BSucc BZero））Nil））
  

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

我们可以编写一些示例代码来试用我们的 add 函数。我们会对 seq 和 hFlush 有点偏执，以便我们可以看到我们的表示有多糟糕

  mseq :: Monad m => a  - > m a 
 mseq a = a`seq`返回一个
 
 runPRF :: PRF n  - >列表n纳特 - > IO（）
 runPRF fi = 
 do 
 putStrLn编译函数
 hFlush stdout 
 f'<  -  mseq $编译f 
 putStrLn正在运行函数
 hFlush stdout 
n<  -  mseq $ f'i 
 print n 
  

如果我们用 add 运行一个例子，我们会得到一个很好的满意输出

  runPRF add（Cons（S（SZ））（Cons（S（S（SZ）））无））
 
编译函数
运行函数
 S（S（S（SZ））））
  

Haskell声明

我们可以用Haskell声明做一些有趣且最终破坏性的事情。首先我们会让模式匹配更容易。如果不提供使用递归结果的函数，就可以使用 PRec 中的模式匹配。 match 会为我们添加额外的虚拟参数。

  match :: （深度列表k）=> PRF k  - > PRF（S k） - > PRF（S k）
匹配fz fs = PRec fz（addArgument（BSucc BZero）fs）
  

<要做到这一点，它需要一个辅助函数，它添加参数 addArgument 和其他一些实用程序来测量已知类型列表的大小， Depths ，比较并转换 BNat s，并证明递增的自然数仍然在新的边界之下。

  { - ＃LANGUAGE MultiParamTypeClasses＃ - } 
 { - ＃LANGUAGE FlexibleContexts＃ - } 
 { - ＃LANGUAGE StandaloneDeriving＃ - } 
 
类深度f（n :: Nat）其中
深度:: fn（BNat n）
 
实例深度列表'Z其中
深度=无
 
实例（深度列表n）=>深度列表（'S n）其中
深度=缺点BZero（fmap BSucc深度）
 
派生实例Eq（BNat n）
派生实例Show（BNat n）
导出实例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 
pd = 
 if d'> = n 
 then Proj（BSucc d）
 else Proj d'
 where d' = bid d 
  

这对于编写完美合理的内容非常有用，例如

  nonZero :: PRF（SZ）
 nonZero =匹配Const（Comp Succ（Cons（Comp Const Nil）Nil））
 
 isZero :: PRF（SZ）
 isZero = match（Comp Succ（Cons Const Nil））（Comp Const Nil）
 
 isOdd :: PRF（SZ）
 isOdd = PRec Const（addArgument BZero isZero）
  

递归Haskell声明

我们也可以编写非常具有破坏性的东西，不仅仅是 undefined 。首先，我们将定义一个，同时使用递归定义构造。我们知道用构建的东西，而不应该存在于原始递归函数的闭包中。

  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（缺点步骤（fmap（Proj。BSucc）深度））
  

这让我们写一个循环，只有一些输入不终止。

  infiniteLoop :: PRF（SZ）
 infiniteLoop = while isOdd（Comp Succ（Cons Succ Nil））
  

如果我们运行这个偶数， Z 或 S（SZ），它终止返回输入。如果我们运行一个奇数，它永远不会结束。

  runPRF infiniteLoop（缺点（SZ）无）
编译函数
运行函数
  

因为我们对 seq 和 hFlush 我们可以肯定，编译后的值是以非常原始的递归函数的形式在周头正常形式中居住的，并且不是简单的 undefined 。这是因为编译步骤并不严格，并且减少到周头正常形式并不会导致头部正常形式的减少。我们可以通过向 compile 添加 seq s来解决这个问题。

  compile（Comp f gs）= f'`seq` gs' `seq` go 
其中
 go = \ ns  - > F' 。 fmap（$ ns）$ gs'
 gs'= fmap编译gs 
 f'=编译f 
编译（PRec fg）= f'`seq` g``seq` h 
其中
h（Cons Z t）= f't 
h（Cons（S n）t）= g'（Cons n（Cons（h（Cons nt））t））
 f'=编译f 
 g'=编译g 
  

这将基本上检查<

  runPRF infiniteLoop（Cons Z Nil）code> PRF 在编译时是有限的。
 
编译函数
 GHC堆栈空间溢出：当前限制为33632字节。 
使用'-K< size>'选项增加它。 
  

收拾

没有任何类型我们已经谈到真正代表一对一的原始递归函数。 PRF a 除了上面定义的递归结构和 undefined 之外的其他内容。它也被同一原始递归函数的多个表示所居住。例如，身份函数有其他的定义，包括前继函数的组成（我没有定义）和后继函数。编译结果， List n Nat - > Nat 被任何具有相同类型的Haskell函数居住，它也包含所有的部分递归函数。

隐藏那里是同一函数的多个表示，我们可以使用Haskell所做的相同技巧：隐藏函数的内部。如果某人可以检查 PRF 的唯一方法是严格编译它并将其应用于某个东西，那么没有人能够区分同一原始递归函数的不同之处。

将GADT转换为类型类型，只导出类和 compile 足以隐藏构造函数。

如果我们扭动头部，可以找到导出的另一个界面并注意到原始递归函数的公理像 Category law， Arrow 没有 arr （实际上它与 arr 相反），以及一种仅限于自然数的有限形式的循环。

这应该足以说服你，这几乎是可能的。无论我们做什么，我们仍会受到额外居民的困扰， undefined 。有关如何使其更好的进一步讨论将属于一个不同的问题，其中包括对它应该如何很好的具体问题。

Is there a way to represent the denotational semantics of primitive recursive functions (PRFs) in Haskell?

解决方案

Sort-of. We can encode primitive recursive functions with a Haskell class or GADT. We can then consider that a primitive recursive function is an equivalence class of the data type. The simplest equivalence is over the Haskell denotation semantics of the interpretation of the PRF. This representation is ultimately going to be inexact due to the denotational semantics of Haskell, but let's explore how close we can get.

Primitive Recursive Functions

We'll use the definition of primitive recursive functions from Wikipedia. A PRF a is a primitive recursive function with arity a, where a is a natural number.

{-# 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 constructs the constant function or arity zero which always returns 0. Succ is the successor function of arity one. Proj constructs the family of projection functions which each picks out one of their arguments after skipping the supplied number of arguments. Comp composes a function with a list of other functions that provide its arguments. PRec builds a function that pattern matches on the first argument. PRec applies the first function to the remaining arguments if the first argument is zero. If the first argument is not zero, it recurses into itself with the predecessor of the first argument as the first argument and returns the result of the second function applied to the predecessor of the first argument, the result of the recursion, and the remaining arguments. This is easier to see in the definition of a compiler from a PRF to a Haskell function.

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

The above require the definitions for a natural number Nat, a natural number bounded by a type-level natural number, BNat, and a list with a type-level known length, 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)

We are now equipped to write our first primitive recursive functions. We'll write two examples for identity and addition.

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

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

Notice that we re-used declarations in Haskell to simplify writing these functions; we re-used ident in the definition of add. Ultimately the ability to use Haskell declarations will allow us to create infinite or non-total recursive structures that we can sneak into the PRF type.

We can write some example code to try out our add function. We'll be a little paranoid about evaluation order with seq and hFlush so that we can see just how wrong our representation is later.

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

If we run an example with add we get a nice, satisfying output

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

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

Haskell Declarations

There are some fun and ultimately disruptive things we can do with Haskell declarations. First we'll make pattern matching easier. It'd be nice to be able to use the pattern matching from PRec without providing a function that uses the recursive result. match will add that extra dummy argument for us.

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

To do this it needs a helper function that adds the argument, addArgument, and a few other utilities to measure the size of a list with a known type, Depths, compare and convert BNats, and prove that the incremented natural numbers are still under the new bound.

{-# 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

This is really helpful when writing perfectly reasonable things like

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)

Recursive Haskell Declarations

We can also write very disruptive things that aren't just undefined. First, we'll define a while construct using recursion. We know that things built with while aren't supposed to exist in the closure of primitive recursive functions.

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

This lets us write a loop that is non-terminating for only some inputs.

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

If we run this for an even number, like Z or S (S Z), it terminates returning the input. If we run it for an odd number, it never finishes.

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

Because we were careful with the seq and hFlush we can be certain that the compiled value was inhabited in week head normal form by something that wasn't a primitive recursive function and wasn't simply undefined. This is because the compile step wasn't strict, and reduction to week head normal form didn't cause reduction all the way to head normal form. We could fix this by adding seqs to compile. I've changed only the two patterns that need it.

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

This will essentially check that the PRF is finite when compiling it.

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

Tidying up

None of the types we have talked about really represent primitive recursive function one-for-one. PRF a is inhabited by other things than the recursive structures defined above and undefined. It's also inhabited by multiple representations of the same primitive recursive functions. For example, the identity function has other definitions, including the composition of the predecessor function (which I didn't define) with the successor function. The result of compile, List n Nat -> Nat, is inhabited by any Haskell function with the same type, which will include all the partial recursive functions as well.

To hide that there are multiple representations of the same function we can use the same trick that Haskell does: hide the internals of the function. If the only way someone can inspect a PRF is to strictly compile it and apply it to something then nobody can tell the difference between the same primitive recursive function represented differently.

Converting our GADT into a typeclass and only exporting the class and compile would be enough to hide the constructors.

Another interface to export could be found if we twist our heads around a bit and notice that the axioms for primitive recursive functions are like the Category laws, Arrow without arr (in fact it has the opposite of arr), and a limited form of looping that only works on natural numbers.

This should be enough to convince you that it is almost possible. No matter what we do, we will still be plagued by an extra inhabitant, undefined. Further discussion of how to make it nice would belong to a different question that includes specific concerns for how it should be nice.

这篇关于表示原始递归函数的指称语义的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！