是否可以在 lambda 演算上实现 returns 一个 n 元组的函数？
Is it possible to implement a function that returns an n-tuple on the lambda calculus?
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 和 returns 任何 N 对应的 N 元组的函数？另外，是否可以扩展此功能，使其也 returns 相应的访问器？ 该算法不能使用任何形式的递归，包括定点组合器。
~
编辑：根据要求，详细说明我的尝试。
我希望该函数不依赖于递归/定点组合器，因此，最明显的方法是使用教堂编号进行重复。话虽如此，我尝试过随机测试许多表情，以了解它们是如何成长的。例如：
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 元组的第 3 个（因为 2 是第 3 个自然元素）元素。
现在，关于元组。请注意，问题是找到一个术语 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。
这就是我到目前为止所尝试的方法。
如果您可以构建 n 元组，则可以轻松访问第 i 个索引。
首先，我们需要一个类型，用于无限的无类型 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 元组的第 i 个索引（第一个索引从 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"
要构造元组，您需要迭代一些函数，将参数添加到函数而不是删除它们。
让
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
returns 其参数的反向列表：
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)
＼＼

让我们尝试实现 n 元元组构造函数。我还将以简单的实现为目标，这意味着我会尝试坚持消除自然数和元组，并尽量避免使用其他（Church 编码）数据结构。
我的策略如下：
- 用相关语言编写函数的类型正确的版本。
- 将其转换为无类型的 lambda 演算。
这样做的原因是，我很快就迷失在无类型的 lambda 演算中，并且在这个过程中我肯定会犯很多错误，而依赖类型的环境让我陷入 rails。此外，证明助手对编写任何类型的代码都非常有帮助。
第一步
我用的是 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 元函数 returning 一个元组。
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 的情况很简单，但是 cons 的情况有点棘手：
nTupCons : ∀ {n} → NTupCons n
nTupCons [] x = x
nTupCons (t ∷ ts) x = ?
我们需要一个 NFun ts (NTup (t ∷ ts)) 来代替问号。我们知道 nTupCons ts 的类型是 NFun ts (NTup ts)，因此我们需要以某种方式从后者获取前者。我们注意到我们需要的只是 n 元函数组合，或者换句话说，NFun:
的 return 类型的函子映射
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)，因为我们已经有了范围内类型为 t 的 x，这很容易：
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 索引（因为我们通过迭代 n 来实现 compN）。所以我们写了一个有点像 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
似乎有效。
我找到了！给你：
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))))))
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 和 returns 任何 N 对应的 N 元组的函数？另外，是否可以扩展此功能，使其也 returns 相应的访问器？ 该算法不能使用任何形式的递归，包括定点组合器。
~
编辑：根据要求，详细说明我的尝试。
我希望该函数不依赖于递归/定点组合器，因此，最明显的方法是使用教堂编号进行重复。话虽如此，我尝试过随机测试许多表情，以了解它们是如何成长的。例如：
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 元组的第 3 个（因为 2 是第 3 个自然元素）元素。
现在，关于元组。请注意，问题是找到一个术语 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。
这就是我到目前为止所尝试的方法。
如果您可以构建 n 元组，则可以轻松访问第 i 个索引。
首先，我们需要一个类型，用于无限的无类型 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 元组的第 i 个索引（第一个索引从 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"
要构造元组，您需要迭代一些函数，将参数添加到函数而不是删除它们。
让
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
returns 其参数的反向列表：
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)
＼＼ 
让我们尝试实现 n 元元组构造函数。我还将以简单的实现为目标，这意味着我会尝试坚持消除自然数和元组，并尽量避免使用其他（Church 编码）数据结构。
我的策略如下：
- 用相关语言编写函数的类型正确的版本。
- 将其转换为无类型的 lambda 演算。
这样做的原因是，我很快就迷失在无类型的 lambda 演算中，并且在这个过程中我肯定会犯很多错误，而依赖类型的环境让我陷入 rails。此外，证明助手对编写任何类型的代码都非常有帮助。
第一步
我用的是 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 元函数 returning 一个元组。
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 的情况很简单，但是 cons 的情况有点棘手：
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)，因为我们已经有了范围内类型为 t 的 x，这很容易：
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 索引（因为我们通过迭代 n 来实现 compN）。所以我们写了一个有点像 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
似乎有效。
我找到了！给你：
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))))))