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

Question

The n-tuple in lambda calculus is usually defined as:

1-tuple: λ at . ta 1-tuple-fst: λ t . t (λ a . a) 2-tuple: λ abt . tab 2-tuple-fst: λ t . t (λ ab . a) 2-tuple-snd: λ t . t (λ ab . b) 3-tuple: λ abct . tabc 3-tuple-fst: λ t . t (λ abc . a) 3-tuple-snd: λ t . t (λ abc . b) 3-tuple-trd: λ t . t (λ abc . c) ... and so on. 

My question is: is it possible to implement a function that gets the church number N and returns the corresponding N-tuple for any N? In addition, is it possible to expand this function so that it also returns the corresponding accessors? The algorithm cannot use any form of recursion, including fixed-point combinators.

~

Edit: on request, clarification of what I tried.

I want this function not to depend on recursion / fixed point combinators, so the obvious way to do this would be to use church numbers for repetition. Said I tried randomly testing a lot of expressions to find out how they grow. For instance:

 church_4 (λ abc . a (bc)) 

Reduces to:

 (λ abcdef . a ((((ed) c) b) a))))) 

I compared the abbreviation of many similar church_4 (λ abc . (a (bc))) combinations church_4 (λ abc . (a (bc))) with my desired results and noticed that I could implement accessors like:

 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 access to the third (because 2 is the 3rd natural) element of the 6-tuple.

Now, on tuples. Note that the problem is finding the my_term member such that, for example:

 church_3 my_term 

had the following normal form:

 (λ abcdt . ((((ta) b) c) d)) 

As you can see, I almost found it because:

 church_3 (λ abc . a (bc)) (λ a . a) 

Reduces to:

 (λ abcd . (((ab) c) d)) 

This is almost the result I need, except that t missing.

Here is what I have tried so far.

Answer 1

Try implementing the n-ary tuple constructor. I will also strive for simple implementation, which means that I try to avoid natural numbers and tuples and try to avoid using other (Church-related) data structures.

My strategy is this:

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

The reason for this is that I quickly get lost in the untyped calculus of lambda, and I have to make a lot of mistakes along the way, while the dependent typed environment puts me on the rails. In addition, troubleshooting assistants are just a great help for writing any code.

Step one

I am using Agda. I'm a little cheating on type-in-type . This makes Agda inconsistent, but suitable types of universes will be a huge pain for this problem, and it is very unlikely that we will encounter inconsistency anyway.

 {-# OPTIONS --type-in-type #-} open import Data.Nat open import Data.Vec 

We need the concept of n-ary polymorphic functions. We store 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. Constructors for n-ary sets are n-ary functions that return a set.

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

We would like to have a function of type ∀ {n} → NTupCons n . We return the Vec Set n parameter for the tuple constructor. The empty case is simple enough, but the case with the ends is a bit more complicated:

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

We need a NFun ts (NTup (t ∷ ts)) instead of a question mark. We know that nTupCons ts is of type NFun ts (NTup ts) , so we need to somehow get the first from the last. We notice that we only need the n-ary composition of the function, or, in other words, the functorial mapping over the returned type of NFun :

 compN : ∀ {n AB} (ts : Vec Set n) → (A → B) → NFun ts A → NFun ts B compN [] f = f compN (t ∷ ts) fgx = compN ts f (gx) 

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

 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) 

Second step

We will get rid of Vec Set n -s and rewrite the functions so that they iterate over the parameters n . However, a simple iteration is not suitable for nTupCons , since it gives us a recursive result ( nTupCons ts ), but we also need the current index n for compN (since we implement compN by iterating over n ). Therefore, we are writing an assistant that is a bit like paramorphism . We also need pairs encoded in churches to pass Nat -s through iteration:

 zero = λ z s. z suc = λ nz s. s (nzs) 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 = λ zfn . fst ( n (λ p. pz zero) (λ hyp p. p (f (fst hyp) (snd hyp)) (suc (snd hyp)))) -- Note: I use "hyp" for "hypothesis". 

The rest can be easily translated:

 compN = λ n. n (λ f. f) (λ hyp fg x. hyp f (gx)) nTupCon = rec-with-n (λ x. x) (λ hyp n. λ x. compN n (λ f g. f (gx)) hyp) 

Test it for simple cases:

 nTupCon zero = (λ t. t) nTupCon (suc zero) = (λ hyp n. λ x. compN n (λ f g. f (gx)) hyp) (nTupCon zero) zero = λ x. compN zero (λ f g. f (gx)) (λ t. t) = λ x. (λ f g. f (gx)) (λ t. t) = λ x. λ g. (λ t. t) (gx) = λ x . λ g. gx = λ xg . gx nTupCon (suc (suc zero)) = (λ hyp n. λ x. compN n (λ f g. f (gx)) hyp) (nTupCon (suc zero)) (suc zero) = λ x. compN (suc zero) (λ f g. f (gx)) (λ a t. ta) = λ x a. (λ f g. f (gx)) ((λ y t. ty) a) = λ x a. (λ f g. f (gx)) (λ t. ta) = λ xa g. (λ t. ta) (gx) = λ xa g. gxa 

This seems to work.

Answer 2

Let be

 foldargs = λ tnfz . (IsZero n) (tz) (λ a . foldargs t (pred n) f (faz)) 

Then the function

 listofargs = λ n . foldargs id n pair null 

returns a reverse list of its arguments:

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

Function

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

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

 apply f [abcde] --> fabcde 

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 other functions can be taken from wikipedia . Recursion can be eliminated by Y-combinator . reverse is simple.

UPD: non-recursive versions of functions:

 foldargs = Y (λ ctnfz . (IsZero n) (tz) (λ a . ct (pred n) f (faz))) apply = Y (λ cfl . (isnil l) f (c (f (head l)) (tail l))) Y = λ f (λ x . fxx) (λ x . fxx) 

 

Answer 3

If you can build n tags, you can easily access the i th index.

First, we need a type for infinite untyped lambda functions. The optional X constructor allows us to test 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 is 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 numbers, you will need some church numbers. We will also need to subtract to figure out how many extra arguments to skip when indexing to tuple 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) 

A constant function returns its first argument. If we iterate a constant function several times, it discards many of the 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 returns the second argument. If we repeat it several times, this reduces the number of 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 the index n tuple i th (starting from zero for the first index), we need to discard the arguments ni-1 from the end and discard the arguments i from the beginning.

 -- drops (ni-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 will define some examples of fixed-size tuples

 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 appropriate accessors can be created.

 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) 

Execution of these outputs

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

To build tuples, you will need to iterate over some function that adds function arguments instead of dropping them.

Answer 4

I found him! There you go:

 nTup = (λ n . (n (λ ftk . (f (λ e . (t (ek))))) (λ 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)))))) 

Etc. It saves the elements back, but I don’t think I will fix it - it looks more natural. The challenge was to get 0 in the left-most inner pair. As I said, I could easily get both (0 (1 (2 (3 4)))) and ((((4 3) 2) 1) 0) , but they do not work as tuples, because 0 is what contains the elements there.

Thanks everyone!

Edit: I really decided with this:

 nTup = (λ a . (a (λ bcd . (b (λ b . (cbd)))) (λ x . x) (λ x . x))) 

Which keeps the correct order.

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