Is it possible to implement a function that returns an n-tuple on the lambda calculus?

Question

An n-tuple on the lambda calculus is usually defined as:

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.

My question is: is it possible to implement a function that receives a church number N and returns the corresponding N-tuple for any N? Also, is it possible to extend this function so it also returns the corresponding accessors? The algorithm can't use any form of recursion, including fixed-point combinators.

~

Edit: as requested, elaborating on what I've tried.

I want that function not to depend on recursion / fixed point combinators, so, the obvious way to do it would be using church-numbers for repetition. Said that, I have tried randomly testing many expressions, in order to learn how they grow. For example:

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

Reduces to:

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

I've compared the reduction of many similar combinations church_4 (λ a b c . (a (b c))) to my desired results and noticed that I could implement the accessors as:

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

Where sub is the subtraction operator and access church_5 church_2 means accessing the 3rd (because 2 is the 3rd natural) element of a 6-tuple.

Now, on the tuples. Notice that the problem is finding a term my_term such that, for example:

church_3 my_term

had the following normal form:

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

As you can see, I've almost found it, since:

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

Reduces to:

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

Which is almost the result I need, except thatt is missing.

That is what I've tried so far.

Answer 1

Let's try to implement the n-ary tuple constructor. I shall also aim for a simple implementation, meaning that I try sticking to the elimination of natural numbers and tuples, and try to avoid using other (Church encoded) data structures.

My strategy is as follows:

1. Write a well-typed version of the function in a dependent language.
2. Translate it to untyped lambda calculus.

The reason for this is that I quickly get lost in untyped lambda calculus and I'm bound to make quite a few mistakes along the way, while the dependently typed environment puts me on rails. Also, proof assistants are just great help for writing any kind of code.

Step one

I use Agda. I cheat a bit with type-in-type. It makes Agda inconsistent, but for this problem proper type universes would be a huge pain, and it's very unlikely that we actually run into an inconsistency here anyway.

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

open import Data.Nat
open import Data.Vec

We need a notion of n-ary polymorphic functions. We store the argument types in a vector of length 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

We have the usual Church encoding for tuples. The constructors for n-ary tuples are n-ary functions returning a tuple.

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

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

We'd like to have a function with type ∀ {n} → NTupCons n. We recurse on the Vec Set n parameter for the tuple constructor. The empty case is simple enough, but the cons case is a bit trickier:

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

We need a NFun ts (NTup (t ∷ ts)) in place of the question mark. We know that nTupCons ts has type NFun ts (NTup ts), so we need to somehow get the former from the latter. We notice that what we need is just n-ary function composition, or in other words a functorial map over the return type of 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)

Now, we only need to get an NTup (t ∷ ts) from an NTup ts, and since we already have x with type t in scope, that's pretty easy:

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)

Step two

We shall get rid of the Vec Set n-s and rewrite the functions so they iterate on the n parameters. However, simple iteration is not good for nTupCons, since that only provides us the recursive result (nTupCons ts), but we also need the current n index for compN (since we implement compN by iterating on n). So we write a helper that's a bit like a paramorphism. We also need Church encoded pairs here to pass up the Nat-s through the iteration:

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". 

The rest is straightforward to translate:

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)

Let's test it for simple cases:

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

It seems to work.

Answer 2

Let

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

Then function

listofargs = λ n . foldargs id n pair null

returns reversed list of its args:

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

Function

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

applies first argument (n-ary function) to arguments taken from the second argument (a list of length n):

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

The rest is easy:

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

where

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

Implementation of the other functions can be taken from wikipedia. Recursion can be eliminated by Y-combinator. reverse is simple.

UPD: Nonrecursive versions of the functions:

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)