是否有可能实现一个在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))

其他功能的实现可以从维基百科中获取.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 2

让我们尝试实现n-ary元组构造函数.我还将针对一个简单的实现,这意味着我尝试坚持消除自然数和元组,并尽量避免使用其他(Church编码)数据结构.

我的策略如下:

1. 以依赖语言编写函数的良好类型版本.
2. 把它翻译成无类型的lambda演算.

这样做的原因是我很快就迷失了无类型的lambda演算,而且我一定会犯很多错误,而依赖类型的环境让我陷入困境.此外,证明助手对编写任何类型的代码都有很大帮助.

第一步

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

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

open import Data.Nat
open import Data.Vec

我们需要一个n元多态函数的概念.我们将参数类型存储在长度为vector的向量中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

我们有通常的教会编码元组.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了元组构造函数的参数.空案例很简单,但缺点是有点棘手:

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 (t ? ts)要从a 获得一个NTup 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,因为它只为我们提供了递归result(nTupCons ts),但我们还需要当前n索引compN(因为我们compN通过迭代实现n).所以我们写了一个有点像paramorphism的助手.我们还需要教会编码对在这里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

它似乎工作.