3

我在 lambda 演算中对自然数的定义如下，这是我的主要目标。

-- Apply a function n times on x
apply = \f -> \n -> \x -> foldr ($) x $ replicate n f

-- Church numbers
churchZero = \f -> id

churchOne = \f -> \x -> apply f 1 x

churchTwo = \f -> \x -> apply f 2 x

churchNatural = \n -> \f -> \x -> apply f n x

然后，下一步是定义运算churchSum符churchMul和churchExp。

churchSum = \n -> \m -> \f -> \x -> n f (m f x)

churchMul = \n -> \m -> \f -> \x -> n (m f) x

churchExp = \n -> \m -> n m

很好，它可以工作，前两个函数很容易推导出来，但求幂则不然。至少对我来说。为了进一步了解，我对 lambda 项进行了 beta 归一化：
(λf.λx. f(f x))(λf.λx f(f x))有效地查看幂运算是正确的。

β减少

所以，我的问题是：我怎么能在不知道的情况下推断出这个 lambda 项？更重要的是，为什么要λ> churchTwo churchTwo检查Haskell类型何时是类型λ> churchTwo :: (b -> b) -> b -> b？在它里面做函数的 beta 归一化吗？

4

1 回答 1

3

你exp的有点倒退：

((\f x -> f$f$f$x) `exp` (\f x -> f$f$x)) (+1) 0 == 8
--      3            ^          2                 = 8???
-- But 2^3 = 8

正确的（-er-ish）版本是

exp n m = m n
((\f x -> f$f$f$x) `exp` (\f x -> f$f$x)) (+1) 0 == 9
--      3            ^          2                 = 9

因为它保持着熟悉的顺序。这并不会真正影响您如何定义exp.

指数是重复乘法：乘以自身的时间。教堂数字表示函数对值的重复应用。因此，是一个将数字乘以 的函数，是重复函数次的函数，并且是基值（乘法的恒等式）。将它们放在一起，然后简化：nmnmchurchMul nnmmchurchOne

-- n^m is the repeated multiplication of 1 by n, m times
exp n m = m (churchMul n) churchOne
-- expand definitions x2; simplify churchOne
exp n m = m (\o f x -> n (o f) x) (\f x -> f x)
-- eta contract x2
exp n m = m (\o f -> n (o f)) (\f -> f)
-- definition of (.), id
exp n m = m (\o -> n . o) id
-- eta contract
exp n m = m (n .) id
-- eta expand
exp n m f = m (n .) id f
-- Assume m has the type forall b. (b -> b) -> b -> b
-- This assumption may actually be false here, because the implicit type of exp
-- does not require that m, n have that type. The difference is that you could define
-- bogus _ _ _ = 0
-- (which isn't a church numeral) and still pass it to exp, which would no longer
-- act like exponentiation:
-- exp n bogus = bogus (n .) id = const 0
-- which also isn't a church numeral

-- Polymorphic functions like m give rise to theorems that can be derived
-- entirely from their types. I used http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi
-- to get this one automatically.
-- Free theorem of the type of m
forall a b (g :: a -> b) (p :: a -> a) (q :: b -> b).
   (forall (x :: a). g (p x) = q (g x)) ->
     (forall (y :: a). g (m p y) = m q (g y))

-- Instantiate g = ($ f), p = (n .), q = n, y = id
  (forall x. (n . x) f = n (x f)) -> (m (n .) id f = m n f)

-- definition of (.)
  (n . x) f = n (x f)
-- so...
  m (n .) id f = m n f
-- transitive property
exp n m f = m n f
-- eta contract
exp n m = m n

上面带有自由定理的东西m实际上是以下参数的严格版本（它可能更好地转换为无类型的 lambda 演算）：

-- m, being a valid numeral, is of the form
m f x = f $ f $ ... $ f $ f $ x

m (n .) id = (n .) $ (n .) $ ... $ (n .) $ (n .) $ id
           = (n .) $ (n .) $ ... $ (n .) $ n . id
           = (n .) $ (n .) $ ... $ (n .) $ n
           = (n .) $ (n .) $ ... $ n . n
           ...
           = n . n . ... . n . n
-- so
m n = n . n . ... . n . n = m (n .) id

至于为什么要churchTwo churchTwo进行类型检查，请注意该表达式中的每次出现都有不同的类型，因为churchTwo它是多态的，并且描述了整个函数系列，而不仅仅是一个。

-- most general type
churchTwo :: forall b. (b -> b) -> (b -> b)
-- Each occurrence of churchTwo can have a different type, so let's give them
-- different names.
-- I'm using underscores because these variables haven't been solved yet
churchTwo0 :: (_b0 -> _b0) -> (_b0 -> _b0)
churchTwo1 :: (_b1 -> _b1) -> (_b1 -> _b1)
churchTwo0 churchTwo1 :: _
-- Since churchTwo0 is being applied, the whole expression must have the
-- type on the right of the arrow
churchTwo0 churchTwo1 :: _b0 -> _b0
-- Since churchTwo0 is being applied to churchTwo1, the left side of the
-- top level arrow in churchTwo0 must be equal to the type of churchTwo1
(_b0 -> _b0) ~ ((_b1 -> _b1) -> (_b1 -> _b1))
-- Therefore...
(_b0 ~ (_b1 -> _b1))
churchTwo0 churchTwo1 :: (_b1 -> _b1) -> (_b1 -> _b1)
-- That's all the constraints we have, so replace the free variables
-- with universally quantified ones
chuchTwo0 churchTwo1 :: forall b. (b -> b) -> (b -> b)
-- (which is the type of a numeral)
于 2017-11-30T04:52:40.573 回答