Following problems come from functional, available on Steam.

Basic

anything

Any term that conforms to Lambda Calculus syntax (1. variable 2. abstraction 3. application) is okay.

identity

x: x

two arguments

x:y: y x

squaring

f:x: f (f x) 

indirection

f:x:y: f y x

Boolean

Definitions:

TRUE = t:f: t
FALSE = t:f: f

IF

p:t:f: p t f

Simple LC has no type system, so programmers need to ensure that p can always evaluate to TRUE / FALSE, then p t f further evaluates to t/ f. If p cannot evaluate to TRUE / FALSE, then p t f will be retained or produce unexpected evaluation behavior.

One thing you can easily notice is: IF P A B ≡ P A B, you can completely omit IF in all occasions where it’s used. This doesn’t change the semantics and can reduce one reduction, but for readability, there’s still reason to keep IF in somewhat complex programs.

NOT

b: b FALSE TRUE

This looks subtly clever. It can be obtained straightforwardly through b: IF b FALSE TRUE → b FALSE TRUE, or directly by utilizing the meaning of TRUE / FALSE - selecting the first/second item.

AND

p:q: p q p

If p = TRUE, then AND p q ≡ q; if p = FALSE, then AND p q ≡ FALSE ≡ p.

OR

p:q: p p q

If p = TRUE, then OR p q ≡ p ≡ TRUE; if p = FALSE, then OR p q ≡ q.

XOR

p:q: p (NOT q) q

Similar to AND, OR, you can draw a truth table to organize your thoughts.

Pair and List

PAIR

x:y:f: f x y

PAIR A B → (x:y:f: f x y) A B → (f: f A B) is an abstraction that: contains A, B in order, waiting for a function f to act on the contained A, B. For example, when A, B are Boolean, f can be AND / OR / … (of course, the syntax doesn’t restrict the shape of f,A,B, if you want to write PAIR TRUE 0 PAIR the interpreter won’t stop you)

FST

p: p TRUE

When p = PAIR A B, p TRUE → (PAIR A B) TRUE → (f: f A B) TRUE → TRUE A B → A. Note that p is a function that can receive a parameter f, here we make it receive the TRUE function to select the first element. In LC, TRUE / FALSE are more appropriately interpreted as selecting the first/second item that follows, rather than expressing the truth/falsity of a proposition. This is meaningful because when we write programs in other high-level languages, if we need a Boolean value X, X’s ultimate utility is often in the selection of then-clause / else-clause.

SND

p: p FALSE

Similar to FST.

simple list

Get the 3rd item from the list (1-indexed):

l: FST ( SND ( SND l ) )

A list is a simple recursive structure. The recursive base is an empty list, represented here by FALSE. The recursive step is adding elements to a list, implemented here using PAIR. e.g. [] ↦ FALSE, 1 ↦ (PAIR 1 FALSE), [1,3] ↦ (PAIR 1 (PAIR 3 FALSE)). Note in the [1,3] example, if viewed from the perspective of adding elements to a list, the head is the item closest to FALSE, the closer to FALSE, the smaller the index, because it was added earlier. Under this interpretation, [1,3] ↦ (PAIR 3 (PAIR 1 FALSE)). However, the game doesn’t adopt this interpretation, but maintains visual alignment with familiar [a,b,..], making the most recently added item - the leftmost item - the head. Keep this in mind when dealing with ascending/descending order problems later.

ANY

For a list containing 3 Boolean values, return TRUE if any item is TRUE, otherwise return FALSE:

(l: IF 
  (OR 
    (FST (SND (SND l))) 
    (OR 
      (FST l) 
      (FST (SND l))
    )
  )
  TRUE FALSE
)

Just write according to logic straightforwardly. Here the list has fixed length, which is easy to deal with. Variable-length lists would require recursion, see later.

PUSH

(m:l: PAIR m l)

Use PUSH to add new item m to list l. According to η-reduction, PUSH ≡ PAIR, so writing PAIR directly is sufficient here.

POP

SND

Pop out the outermost / leftmost item.

EMPTY

l: l (t:x:y: FALSE) TRUE

First, EMPTY needs to receive a list, so its basic shape is EMPTY = l: ....

Consider case l' = FALSE, EMPTY l' ~expected→ TRUE. Using FALSE’s selection ability, we make EMPTY = l: l 𝕏 TRUE.

Consider case l* = PAIR a (PAIR b (...)) = (f: f a (PAIR b (...))) ≈ (f: f a _tail), viewing l* as a function receiving one parameter, EMPTY l* = (f: f a _tail) 𝕏 TRUE → 𝕏 a _tail TRUE ~expected→ FALSE. Then 𝕏’s job is to receive the following 3 items and return FALSE, so 𝕏 = (t:x:y: FALSE).

Combining all above gives the final solution EMPTY = l: l (t:x:y: FALSE) TRUE

Recursion

create recursion - Y combinator

Motivation: Recursion in LC

Try to define recursive factorial function in LC:

f = a: IF (EQ a 1)
     1
     (a * f (a - 1))

The above definition doesn’t conform to LC syntax because LC functions are anonymous functions and don’t support calling functions by name (like f above). Yet recursive functions inevitably need self-reference. How to solve this problem?

Applying function $F$ to parameter $A$ can be expressed as $F A$, or using higher-order functions like this: $(\lambda fa.\ f\ a) F A$. Building on this, add some logic, like expressing “with parameters $a$ and $p$, function $f$, if $p\ a$ is true, return $f\ a$, otherwise return $a$ itself”: $(\lambda fap.\ IF\ (p\ a)\ (f\ a)\ a)$. Based on this idea, assuming our target factorial function is F, then F satisfies this equation, denoting (f:a: ..) as F':

F = (f:a: IF (EQ a 1)
      1 
      (a * f (a - 1))
  )  F 
  ≡ F' F 

Looking at the right side of the equation, F'’s meaning is to receive function f and parameter a, if EQ a 1 return 1, otherwise return a * f (a - 1). Passing recursive function F to F', the behavior of resulting function F' F matches our target factorial function F, semantically making both sides equal.

Currently we have equation F = F' F ①, where F' is a known closed term. Since F involves self-reference, no normal form exists, so consider if there exists some Y s.t. Y F' = F ②. Substituting ② into ①, we get Y F' = F' (Y F'). The next goal is to solve for Y’s normal form. Once we get Y, target recursive function F = Y F' follows.

Designing the Y Combinator

Y is a term that satisfies: Y F = F (Y F) = F (F (Y F)) = .... (Note: How/When the term expands depends on the evaluaton strategy.)

To design Y that meets the above requirements, let’s analyze:

1. Y must be of the form (f: ...).

2. Self-reference in Y? — We need to repeat Y, or construct the right-side Y.

   Function/Abstraction is All You Need — Since LC has no storage, in Y F = F (Y F), the Ys on both sides aren’t the same instance. They’re not value or address copies (LC has no storage concept). The right-side Y needs to be constructed, being equal under alpha-conversion to the left-side Y.

3. How to repeat F? Simple - Y = (f: ...) receives parameter F, and within Y’s body, we can repeat it as needed.

4. Design an abstraction M for construction. M will receive necessary parameters and organize them to form a structure identical to Y.

   1. Y = f: M f ... ~ᴇxᴘᴇᴄᴛᴇᴅ→ M = f: f (Wai f): M needs Y’s parameter f and must build structure matching Y F;
   2. Y = f: M f M ... ~ᴇxᴘᴇᴄᴛᴇᴅ→ M = f:m: f (m f m): Since we want M to match Y F’s structure, and Y contains M, M must contain M too, passed via parameter m. In M’s body, leftmost f implements f’s reapplication, (m f m) constructs structure alpha-equivalent to left-side Y F.
   3. Y = f: M f M, where M = f:m: f (m f m) is a valid Y combinator, verifiable by Y F = M F M = (f:m: f (m f m)) F M = F (M F M) = F (M F M) = F (Y F).

5. There are countless Y combinators, like (a) Y = f: M M f, M = m:f: f (m m f) - similar but more concise via η-reduction to Y = M M, M = ..., as given by Turing; (b) Y = f: E (E f) E f, E = r:s:f: f (s r s f) works too but less elegant; (c) most concise Y = f: (x: f (x x)) (x: f (x x)) which differs by not containing combinator sub-terms.

• Exercise: How to implement combinator D satisfying D F D = D (D F D) D = ...?

  One solution: D = f:d: d (d f d) d, following similar principles.

• Must Y be a combinator? Can it have free variables?

  If Y had free variable z, constructing Y with M must consider z:

  1. closed M: Pass z as parameter giving Y = f: M f c M, M = f:c:m: f (m f c m) - works but adds unnecessary complexity;
  2. open M: If M contains free z, like Y = f: K f K z, K = f:k: f (k f k z), it fails producing: Y F = F (K F K z) z = F (Y F) z = F (F (Y F) z) z.

  Conclusion: Possible but pointless. Intuitively, arbitrary free variables serve no purpose.

Using the Y combinator

Following the motivation section, we use F' = f:a: ... to express the application logic between recursive function f and its parameter a. With target recursive function F, we have F = F' F. Since self-reference is invalid, we consider using Y F' to represent F. In the previous section we derived a viable Y, so F = Y F' gives us our desired target function.

The problems in this section become straightforward once you understand the Y combinator. Key points to note:

1. When using previously defined functions, pay attention to parameter order. For example, FILTER takes the list first, then the filtering function. Since Simple LC has few syntax constraints, programmers need to be extra careful;
2. Several problems may involve list reversal, so write REVERSE first and reuse it;
3. Watch your bracket matching - write in an advanced editor first to avoid basic errors, then copy the code into the game for evaluation. The answers below pass evaluation but may not be the most concise.

strip prefix

Remove FALSE prefix from variable length list:

Y (f:l:
    IF 
    (FST l)
    l 
    (f (SND l))
    )

ACC

Y  (a:l:f:i: 
    IF (EMPTY l)
    i 
    (a (SND l) f (f i (FST l))) 
    )

ALL

l: ACC l AND TRUE

REVERSE

Y (i:c:l: 
    IF 
    (EMPTY l) 
    c 
    (i (PAIR (FST l) c) (SND l))
    ) 
    FALSE 

MAP

Y  (m:c:l:f:
        IF 
        (EMPTY l)
        (REVERSE c)
        (m (PAIR (f (FST l)) c)  (SND l) f) 
    )
FALSE

NONE

(l: ALL (MAP l NOT))

FILTER

Y (m:c:l:f:
        IF 
        (EMPTY l)
        (REVERSE c)
        (   IF 
        (f (FST l))
        (m (PAIR (FST l) c) (SND l) f) 
        (m c (SND l) f)
        )
    )
    FALSE

ZIP

Y (z:c:m:n:
    IF 
    (EMPTY m)
    (REVERSE c)    
    (z (PAIR (PAIR (FST m) (FST n)) c) (SND m) (SND n)) 
    ) 
    FALSE

EQBLIST

(m:n: ALL 
    (MAP 
        (MAP 
        (ZIP m n) 
        (p: XOR (FST p) (SND p))
        ) 
        NOT
    ) 
)

CONCAT

(m:n: 
    (Y (g:c:r:
        IF (EMPTY r)
        c
        (g (PAIR (FST r) c) (SND r))
        )
    )
    n (REVERSE m) 
)

Numerals

Church Numerals use functions to express natural numbers. Two key points are: 1. base (0 := f:x: x) 2. successor (SUC). By repeatedly applying successor to the base, we can obtain all Church Numerals.

SUC

Given Church Numeral n, n is a function that takes parameters f, x, where n f x means applying f to x $n$ times. SUC n is a function that takes f, x and applies f to x $(n+1)$ times.

(n: (f:x: f (n f x) ) )

ZERO

Use logical operations to determine if given n is (f:x: x).

(n: n (x: AND FALSE x) TRUE)

PRE

A basic observation is n = n SUC 0, where equality means intensional equality. So iterating on PAIR 0 0 $n$ times, where each iteration: 1. aligns right number with left 2. increments left number, means right number always lags left by one step. After $n$ iterations, left number is n, right number is its predecessor.

(n: SND (n (p: PAIR (SUC (FST p)) (FST p)) (PAIR 0 0) ) )

ADD

Given x, y, the goal is x+y, meaning: ready to receive f, z, apply f to z $(x+y)$ times. First apply f to z $x$ times getting x f z, then apply f to (x f z) $y$ times.

(x:y: (f:z: y f (x f z)) )

SUB

(x:y: (f:z: (y PRE x) f z))

MUL

(x:y:f:z: y (x f) z )

DIV

(Y (d:c:x:y:
    IF (ZERO x)
    0    
    ( 
      IF (ZERO (y PRE x))
      (SUC c)
      (d (SUC c) (y PRE x) y)
    ) 
   ) 
) 0

EQ

(x:y: AND 
    (ZERO (x PRE y)) 
    (ZERO (y PRE x))
)

MIN

(x:y: IF (ZERO (x PRE y))
      y
      x
)

MAX

(x:y: IF (ZERO (x PRE y))
      x
      y
)

More Numerals

is odd

(n: (n NOT FALSE))

As a side note, here’s a recursive method for checking odd/even numbers (looks interesting, fresher than familiar mod 2):

isEven :: Int -> Bool 
isEven 0 = True 
isEven x = isOdd (x-1)

isOdd :: Int -> Bool
isOdd 0 = False
isOdd x = isEven (x-1)

increasing list

Tail recursive:

(Y (f:c:n: IF (ZERO n)
           (PAIR 0 c)
           (f (PAIR n c) (PRE n))
   ) 
) FALSE

Non-tail recursive:

(n: REVERSE 
    ( 
     (Y (f:x: 
            IF (ZERO x)
            (PAIR 0 FALSE)
            (PAIR x (f (PRE x))))
     ) n
    )
)

decomposition

Decompose given number into sum of powers of 2:

(Y (f:c:k:n:
     IF (ZERO n)
     c
     (IF (AND (EQ n (MIN k n)) (NOT (EQ k n)))  
         (f c (DIV k 2) n)
         (f (PAIR k c) (DIV k 2) (SUB n k) )
     )
   )
) FALSE 8

* primes and sort both need significant runtime (local tests show around 30min each level)

primes

Y (f:l:p:n: 
     IF (EQ n (FST p)) 
     (PAIR n l)
     (IF (EQ (FST p) (MAX n (FST p)))
      (f l (SND p) n)
      ( IF (
            (Y (f:n:p:
                IF (EQ n (MIN n p) )
                (IF (EQ n p) TRUE FALSE )
                (f (SUB n p) p)   
               )
            ) n (FST p)
           )
        (f (PAIR (FST p) l) p (DIV n (FST p)))
        (f l (SND p) n)
      )
     )
  )
  FALSE
  (PAIR 47 (PAIR 43 (PAIR 41 (PAIR 37 (PAIR 31 (PAIR 29 
  (PAIR 23 (PAIR 19 (PAIR 17 (PAIR 13 (PAIR 11 (PAIR 7 
  (PAIR 3  (PAIR 2 FALSE))))))))))))))

sort

Selection sort:

Y (f:c:l: 
    IF (EMPTY l)
    c
    (
        (m: (f (PAIR m c) (FILTER l (x: NOT (EQ x m)) )) ) 
        (ACC l MAX 0)
    )
  ) FALSE

trees

NODE

l:v:r:f: f l v r

LEF

t: t (l:v:r: l) 

RIG

t: t (l:v:r: r)

VAL

t: t (l:v:r: v)

BEMPTY

Similar to checking empty list. Non-empty trees have the form of NODE l v r = f: f l v r,and empty tree is represented by FALSE := a:b: b. Using a tree t as a function: if empty tree, t A B = FALSE A B = B ~ᴇxᴘᴇᴄᴛᴇᴅ→ TRUE, if non-empty t A B = (f: f l v r) A B = A l v r B ~ᴇxᴘᴇᴄᴛᴇᴅ→ FALSE. Thus with B = TRUE, A = l:v:r:x: FALSE:

(t: t (l:v:r:x: FALSE) TRUE )

FIND

Check if tree t contains node with value v:

Y (f:t:v:
    IF (BEMPTY t)
    FALSE
    (IF (EQ (VAL t) v)
     TRUE
     (OR (f (LEF t) v) (f (RIG t) v))    
    )
  )

BSIZE

Calculate tree size:

Y (f:t:
    IF (BEMPTY t)
    0
    (SUC (ADD (f (LEF t)) (f (RIG t))))
  )

BUILD

Binary search tree construction:

Y (f:c:l:
    IF (EMPTY l)
    c
    (   f
        (
          (
          Y (f:v:t:
              IF (BEMPTY t)
              (NODE FALSE v FALSE)
              ( IF (EQ v (MIN v (VAL t)))
                (NODE (f v (LEF t)) (VAL t) (RIG t))
                (NODE (LEF t) (VAL t) (f v (RIG t)))
              )
            )
          )           
          (FST l) c)
        (SND l)
    ) 
  ) FALSE

[ Seems like PREORDER and INORDER functions are swapped in the game? ]

PREORDER

Inorder traversal of binary tree:

Y (f:t: 
    IF (BEMPTY t)
    FALSE
    (CONCAT (f (LEF t))
        (PUSH (VAL t)  
              (f (RIG t))
        )
    )
  )

INORDER

Preorder traversal of binary tree:

Y (f:t: 
    IF (BEMPTY t)
    FALSE
    (PUSH (VAL t)
        (CONCAT (f (LEF t)) 
                (f (RIG t))
        )
    )
  )

SPLIT

Split tree t using value v as boundary:

Y (f:t:v:
    IF (BEMPTY t)
    (PAIR FALSE FALSE)
    (
      IF (EQ v (MAX v (VAL t)))
      (
        (p: PAIR (NODE (LEF t) (VAL t) (FST p)) (SND p)) 
        (f (RIG t) v)
      )
      (
        (p: (PAIR (FST p) (NODE (SND p) (VAL t) (RIG t) ))) 
        (f (LEF t) v)
      )
    )
  )

KTH

Find kth largest element in given binary search tree by getting kth item from inorder traversal list:

(t:k: 
    Y (f:c:l:
        IF (EQ c 0)
        (FST l)
        (f (PRE c) (SND l) )
    ) k (PREORDER t)
)

inverse 6

For given binary search tree t, find missing numbers from [1..6] in ascending order:

t: 
  IF (BEMPTY t)
  (PAIR 1 (PAIR 2 (PAIR 3 (PAIR 4 (PAIR 5 (PAIR 6 FALSE))))))
  (
   Y (f:c:m:n:
        IF (EMPTY n)
        (REVERSE c)
        (
          IF (EQ (FST m) (FST n))
          (f c (SND m) (SND n))
          (f (PAIR (FST n) c) m (SND n))
        )
    ) 
    FALSE
    (PREORDER t)
    (PAIR 1 (PAIR 2 (PAIR 3 (PAIR 4 (PAIR 5 (PAIR 6 FALSE))))))
  )