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

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)

 

Answer 2

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 3

I found it! There you go:

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

Testing:

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

And so on. It stores the elements backwards but I don't think I'm gonna fix that - it looks more natural like so. The challenge was getting that 0 on the leftmost innermost paren. As I said, I could easily get both (0 (1 (2 (3 4)))) and ((((4 3) 2) 1) 0), but those don't work as tuples because that 0 is what holds the elements there.

Thank you all!

Edit: I've actually settled with this one:

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

Which preserves the correct order.

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

Answer 4

If you can construct the n-tuples, you can easily access the ith index.

First, we need a type for the otherwise infinite untyped lambda functions. The extra X constructor allows us to inspect these functions by executing them.

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"

It's convenient to be able to apply functions to each other.

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

infixl 1 `ap`

If you are going to encode numbers with Church numerals you need some church numerals. We will also need subtraction to figure out how many additional arguments to skip when indexing into an n tuple.

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)

The constant function drops its first argument. If we iterate the constant function some numeral number of times, it drops that many first arguments.

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

We can make another constant function that drops its second argument. If we iterate it some numeral number of times, it drops that many second arguments.

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

To index into an n tuple's ith index (starting at zero for the first index), we need to drop n-i-1 arguments off the end and drop i arguments off the start.

-- 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)

We'll define few example tuples of fixed size

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

which we can use to demonstrate that it is possible to generate the corresponding accessors.

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)

Running this outputs

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

To construct tuples you will need to iterate some function that adds arguments to a function instead of dropping them.