是否可以实现一个在 lambda 演算上返回 n 元组的函数？

Question

lambda 演算上的 n 元组通常定义为：

1-tuple:     λ a t . t a
1-tuple-fst: λ t . t (λ a . a)

2-tuple:     λ a b t . t a b
2-tuple-fst: λ t . t (λ a b . a)
2-tuple-snd: λ t . t (λ a b . b)

3-tuple:     λ a b c t . t a b c
3-tuple-fst: λ t . t (λ a b c . a)
3-tuple-snd: λ t . t (λ a b c . b)
3-tuple-trd: λ t . t (λ a b c . c)

... and so on.

我的问题是：是否有可能实现一个函数，接收一个教堂号码N 并为任何 N 返回相应的 N 元组？此外，是否可以扩展此函数以便它也返回相应的访问器？ 该算法不能使用任何形式的递归，包括定点组合器。

~

编辑：根据要求，详细说明我的尝试。

我希望该功能不依赖于递归/定点组合器，因此，显而易见的方法是使用教堂编号进行重复。话虽如此，我已经尝试随机测试许多表达式，以了解它们是如何成长的。例如：

church_4 (λ a b c . a (b c))

减少到：

(λ a b c d e f . a ((((e d) c) b) a)))))

我比较了许多相似组合 church_4 (λ a b c . (a (b c))) 的减少与我想要的结果，并注意到我可以将访问器实现为：

firstOf = (λ max n . (firstOf (sub max n) (firstOf n)))
access = (λ max idx t . (t (firstOf (sub max idx) (firstOf idx))))

sub 是减法运算符，access church_5 church_2 表示访问 6 元组的第三个（因为 2 是自然的第三个）元素。

现在，关于元组。请注意，问题在于找到一个术语my_term，例如：

church_3 my_term

有以下范式：

(λ a b c d t . ((((t a) b) c) d))

如你所见，我几乎找到了它，因为：

church_3 (λ a b c . a (b c)) (λ a . a)

减少到：

(λ a b c d . (((a b) c) d))

这几乎是我需要的结果，只是缺少t。

这是我迄今为止所尝试的。

Answer 1

让我们尝试实现 n 元组构造函数。我还将以简单的实现为目标，这意味着我尝试坚持消除自然数和元组，并尽量避免使用其他（Church 编码的）数据结构。

我的策略如下：

1. 用依赖语言编写函数的类型良好的版本。
2. 将其转换为无类型的 lambda 演算。

原因是我很快就迷失在无类型的 lambda 演算中，并且在此过程中我一定会犯很多错误，而依赖类型的环境让我陷入困境。此外，证明助手对于编写任何类型的代码都非常有帮助。

第一步

我使用 Agda。我对type-in-type 有点作弊。它使 Agda 不一致，但是对于这个问题，正确的类型宇宙将是一个巨大的痛苦，而且我们实际上不太可能在这里遇到不一致。

{-# OPTIONS --type-in-type #-}

open import Data.Nat
open import Data.Vec

我们需要一个 n 元多态函数的概念。我们将参数类型存储在长度为 n 的向量中：

NFun : ∀ {n} → Vec Set n → Set → Set
NFun []       r = r
NFun (x ∷ ts) r = x → NFun ts r
-- for example, NFun (Nat ∷ Nat ∷ []) = λ r → Nat → Nat → r

我们对元组使用通常的 Church 编码。 n 元组的构造函数是返回元组的 n 元函数。

NTup : ∀ {n} → Vec Set n → Set
NTup ts = ∀ {r} → NFun ts r → r

NTupCons : ℕ → Set
NTupCons n = ∀ ts → NFun {n} ts (NTup ts)

我们想要一个类型为∀ {n} → NTupCons n 的函数。我们对元组构造函数的Vec Set n 参数进行递归。 empty case 很简单，但是 cons case 有点棘手：

nTupCons : ∀ {n} → NTupCons n
nTupCons []       x = x
nTupCons (t ∷ ts) x = ?

我们需要一个NFun ts (NTup (t ∷ ts)) 来代替问号。我们知道nTupCons ts 有NFun ts (NTup ts) 类型，所以我们需要以某种方式从后者获取前者。我们注意到我们需要的只是 n 元函数组合，或者换句话说，返回类型为 NFun 的函数映射：

compN : ∀ {n A B} (ts : Vec Set n) → (A → B) → NFun ts A → NFun ts B
compN []       f     = f
compN (t ∷ ts) f g x = compN ts f (g x)

现在，我们只需要从NTup ts 中获取NTup (t ∷ ts)，因为我们已经有了x 范围内的t 类型，这很容易：

nTupCons : ∀ {n} → NTupCons n
nTupCons []       x = x
nTupCons (t ∷ ts) x = compN ts consTup (nTupCons ts)
  where
  consTup : NTup ts → NTup (t ∷ ts)
  consTup tup con = tup (con x)

第二步

我们将摆脱Vec Set n-s 并重写函数，以便它们迭代n 参数。然而，简单的迭代对nTupCons 来说并不好，因为它只为我们提供了递归结果（nTupCons ts），但我们还需要compN 的当前n 索引（因为我们通过迭代实现compN n)。所以我们编写了一个有点像paramorphism 的助手。我们还需要 Church 编码的对来通过迭代传递 Nat-s：

zero = λ z s. z
suc  = λ n z s. s (n z s)
fst  = λ p. p (λ a b. a)
snd  = λ p. p (λ a b. b)

-- Simple iteration has type 
-- ∀ {A} → A → (A → A) → Nat → A

-- In contrast, we may imagine rec-with-n having the following type
-- ∀ {A} → A → (A → Nat → A) → Nat → A
-- We also pass the Nat index of the hypothesis to the "cons" case

rec-with-n = λ z f n . 
  fst (
    n 
      (λ p. p z zero)
      (λ hyp p. p (f (fst hyp) (snd hyp)) (suc (snd hyp))))

-- Note: I use "hyp" for "hypothesis". 

剩下的就直接翻译了：

compN = λ n. n (λ f. f) (λ hyp f g x. hyp f (g x))

nTupCon = 
  rec-with-n
    (λ x. x)
    (λ hyp n. λ x. compN n (λ f g. f (g x)) hyp)

让我们测试一下简单的情况：

nTupCon zero = 
(λ t. t)

nTupCon (suc zero) =
(λ hyp n. λ x. compN n (λ f g. f (g x)) hyp) (nTupCon zero) zero =
λ x. compN zero (λ f g. f (g x)) (λ t. t) =
λ x. (λ f g. f (g x)) (λ t. t) =
λ x. λ g. (λ t. t) (g x) =
λ x . λ g. g x =
λ x g . g x

nTupCon (suc (suc zero)) =
(λ hyp n. λ x. compN n (λ f g. f (g x)) hyp) (nTupCon (suc zero)) (suc zero) =
λ x. compN (suc zero) (λ f g. f (g x)) (λ a t. t a) =
λ x a. (λ f g. f (g x)) ((λ y t. t y) a) =
λ x a. (λ f g. f (g x)) (λ t. t a) =
λ x a g. (λ t. t a) (g x) =
λ x a g. g x a

它似乎有效。

Answer 2

让

foldargs = λ t n f z . (IsZero n) (t z) (λ a . foldargs t (pred n) f (f a z))

然后函数

listofargs = λ n . foldargs id n pair null

返回其参数的反向列表：

listofargs 5 a b c d e --> (e . (d . (c . (b . (a . null))))) or [e d c b a]

功能

apply = λ f l . (isnil l) f (apply (f (head l)) (tail l))

将第一个参数（n 元函数）应用于取自第二个参数（长度为 n 的列表）的参数：

apply f [a b c d e]  --> f a b c d e

剩下的很简单：

n-tuple = λ n . foldargs n-tuple' (Succ n) pair null 

在哪里

n-tuple' = λ l . apply (head l) (reverse (tail l))

其他功能的实现可以参考wikipedia。 Y-combinator 可以消除递归。 reverse 很简单。

UPD：函数的非递归版本：

foldargs = Y (λ c t n f z . (IsZero n) (t z) (λ a . c t (pred n) f (f a z)))
apply = Y (λ c f l . (isnil l) f (c (f (head l)) (tail l)))
Y = λ f (λ x . f x x) (λ x . f x x)

 

Answer 3

我找到了！给你：

nTup = (λ n . (n (λ f t k . (f (λ e . (t (e k))))) (λ x . x) (λ x . x)))

测试：

nTup n1 → (λ (λ (0 1)))
nTup n2 → (λ (λ (λ ((0 1) 2))))
nTup n3 → (λ (λ (λ (λ (((0 1) 2) 3)))))
nTup n4 → (λ (λ (λ (λ (λ ((((0 1) 2) 3) 4))))))

等等。它向后存储元素，但我认为我不会修复它 - 它看起来更自然。挑战是在最左边的最里面的括号上获得那个 0。正如我所说，我可以轻松获得(0 (1 (2 (3 4)))) 和((((4 3) 2) 1) 0)，但它们不能作为元组工作，因为0 是其中的元素。

谢谢大家！

编辑：我实际上已经解决了这个问题：

nTup = (λ a . (a (λ b c d . (b (λ b . (c b d)))) (λ x . x) (λ x . x)))

保留正确的顺序。

nTup n4 → (λ (λ (λ (λ (λ ((((0 4) 3) 2) 1))))))

Answer 4

如果可以构造n-tuples，就可以轻松访问ith 索引。

首先，我们需要一个用于其他无限无类型 lambda 函数的类型。额外的X 构造函数允许我们通过执行这些函数来检查它们。

import Prelude hiding (succ, pred)

data Value x = X x | F (Value x -> Value x)

instance (Show x) => Show (Value x) where
    show (X x) = "X " ++ show x
    show _     = "F"

能够互相应用函数很方便。

ap :: Value x -> Value x -> Value x
ap (F f) = f
ap _     = error "Attempt to apply Value"

infixl 1 `ap`

如果您要使用教堂数字对数字进行编码，则需要一些教堂数字。我们还需要减法来计算在索引到 n 元组时要跳过多少额外参数。

idF = F $ \x -> x

zero = F $ \f -> idF
succ = F $ \n -> F $ \f -> F $ \x -> f `ap` (n `ap` f `ap` x)

one = succ `ap` zero
two = succ `ap` one
three = succ `ap` two
four = succ `ap` three

pred = F $ \n -> F $ \f -> F $ \x -> n `ap` (F $ \g -> F $ \h -> h `ap` (g `ap` f)) `ap` (F $ \u -> x) `ap` idF

subtractF = F $ \n -> (n `ap` pred)

常量函数删除了它的第一个参数。如果我们将常量函数迭代若干次，它会丢弃那么多的第一个参数。

--drops the first argument
constF = F $ \f -> F $ \x -> f
-- drops i first arguments
constN = F $ \i -> i `ap` constF

我们可以创建另一个常量函数，去掉它的第二个参数。如果我们对它进行多次迭代，它会丢弃那么多的第二个参数。

-- drops the second argument
constF' = F $ \f -> F $ \a -> F $ \b -> f `ap` a
-- drops n second arguments
constN' = F $ \n -> n `ap` constF'

要索引到 n 元组的 ith 索引（第一个索引从 zero 开始），我们需要从末尾删除 n-i-1 参数并从开头删除 i 参数。

-- drops (n-i-1) last arguments and i first arguments
access = F $ \n -> F $ \i -> constN `ap` i `ap` (constN' `ap` (subtractF `ap` (succ `ap` i) `ap` n) `ap` idF)

我们将定义几个固定大小的示例元组

tuple1 = F $ \a ->                     F $ \t -> t `ap` a
tuple2 = F $ \a -> F $ \b           -> F $ \t -> t `ap` a `ap` b
tuple3 = F $ \a -> F $ \b -> F $ \c -> F $ \t -> t `ap` a `ap` b `ap` c

我们可以用它来证明可以生成相应的访问器。

main = do
    print $ tuple1 `ap` (X "Example")           `ap` (access `ap` one `ap` zero)

    print $ tuple2 `ap` (X "Hello") `ap` (X "World") `ap` (access `ap` two `ap` zero)
    print $ tuple2 `ap` (X "Hello") `ap` (X "World") `ap` (access `ap` two `ap` one)

    print $ tuple3 `ap` (X "Goodbye") `ap` (X "Cruel") `ap` (X "World") `ap` (access `ap` three `ap` zero)
    print $ tuple3 `ap` (X "Goodbye") `ap` (X "Cruel") `ap` (X "World") `ap` (access `ap` three `ap` one)
    print $ tuple3 `ap` (X "Goodbye") `ap` (X "Cruel") `ap` (X "World") `ap` (access `ap` three `ap` two)

运行这个输出

X "Example"
X "Hello"
X "World"
X "Goodbye"
X "Cruel"
X "World"

要构造元组，您需要迭代一些向函数添加参数而不是删除参数的函数。