haskell - 是否可以实现一个在 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 元组的第 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不见了。

这就是我到目前为止所尝试的。

Answer 1

让

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

返回其 args 的反向列表:

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)