functional: Level PRE Guide (Hints and Solutions)

The PRE level in the numerals chapter is pretty challenging, and the answer is rather complex, so here are a few hints to reduce its difficulty down to “reasonably challenging.” In addition, there are two masked solutions in the end. Spoiler warning!!!

Sketch the shape

Our goal is to construct a function PRE such that:

when n = 0, PRE n = f:x: x,
when n > 0, PRE n = f:x: f^(n-1) x.

Note: the “-” in the exponent is just a denotation, as we can not define “SUB” in lambda calculus at the moment.
PRE could be sketched in many forms. Here we take a lazy guess that it could look like n:f:x: P. Then the next problem is what’s inside P?
Note that n is actually a function that takes two arguments. So, by the strategy you learned from the level EMPTY, we could first feed it two unknown arguments and then construct them. So here we make another guess that P looks like (… n A B …). In summary, the shape of PRE is

n:f:x: (... n A B ...)

It’s not that easy

You might be tempted to let (n A B) equal (f^(n-1) x), then find out it is impossible. Actually, you can prove it is impossible. But a minor tweak could make this strategy work: let’s try letting (n A B) equal to some function with (f^(n-1) x) in its body, then feed (n A B) with an argument C to extract (f^(n-1) x). So the shape of PRE is

n:f:x: (... n A B C ...)

Now you could stop reading and try it out. (It’s still very challenging, though).

Continuation-passing

I know it’s tough, so here are two more detailed skeletons for you. Each leads to one solution.

Try to construct A and B, so that when n > 0,
```
n A B = u: u (f^(n-1) x)
```
Try to construct A and B, so that when n > 0,
```
n A B = u: u (f^(n-1) x) S
```
and when n = 0,
```
n A B = u: u x S'
```
Here S and S’ are something you need to construct.

I suggest you begin with trying the first skeleton, as the second one results in a more complex answer. Besides, there could exist other solutions, so no need to be frustrated if you followed a different path.

The continuation-passing style is a pretty pervasive concept in functional programming. But, unfortunately, the game did not introduce it. So if you have spent hours banging your head against the wall trying to solve this puzzle, you have my sincere condolences.

Solution one

With the goal in mind, we can construct C, B then A in order.

Construct C

For any n > 0, (n A B) should equal (u: u (f^(n-1) x)), so to make (n A B C) equal (f^(n-1) x), C must be identity function (z:z).

Construct B

When n = 0, n A B C = B C. We want it to equal x, so B has to be (u:x).

Construct A

Now constructing A is reasonably challenging. I think its difficulty is the same as solving Y-combinator. You should try it out by yourself.

For any k > 0,

k A B = u: u (f^(k-1) x),
(k+1) A B = v: v (f^k x).

(k+1) A B could also be written as

A (k A B)
= A (u: u (f^(k-1) x)
= ...
= v: v (f^k x)

To let it equal v: v (f^k x), A at least has to be a function. We could make another lazy guess that A’s shape is (g:v: v (… g …)), to match with the final form v: v (f^k x).
Now

A (u: u (f^(k-1) x)
= (g:v: v (... g ...)) (u: u (f^(k-1) x)
= v: v (... (u: u (f^(k-1) x) ...)
= ...
= v: v (f^k x)

Now the answer is obvious, A is (g:v: v (g f)).
You should double-check what happens when n = 1. Fortunately, 1 A B = x.
So the answer is

n:f:x: n (g:v: v (g f)) (u:x) (z:z)

Solution two

Note (u: u (f^(n-1) x) S) is another way of saying (PAIR (f^(n-1) x) S), so I’ll use pair notation to be less wordy.
Let’s restate the skeleton:
We want to construct A and B, so that

When n > 0, n A B = (f^(n-1) x, S)
When n = 0, n A B = B = (x, S')

Let’s call S and S’ selectors.

Construct B

We already found B by setting n = 0.

Construct C

It’s not hard to notice that (n A B) always returns a pair of value and a selector. We then use C to extract this value. Recall that how you implemented FST, you could easily find out C is (a:b:a) which is TRUE.

Construct A

If you tried to solve A by yourself, you’ll probably notice a strange phenomenon. When applying A to a pair, sometimes it adds f to the pair’s first component, sometimes it does not.
For any k > 0,

(k+1) A B
= A (k A B)
= A (f^(k-1) x, S)
= ...
= (f^k x, S)

So A should add f to the first component of a pair.
But when k = 0,

1 A B
= A B
= A (x, S')
= ...
= (x, S)

So A no longer adds f.
The trick is to use the second component, i.e., S and S’, to guide A’s behavior.
You should try it out by yourself.

A at least must be a function that takes a pair as its argument. So A is shaped like (p: …). Also, as I said, we’ll use S and S’ to guide A’s behavior, which means we’ll use (SND p) to select between two choices.
But how to define these selectors? You could use FST and SND to select one component from a pair, or use TRUE and FALSE to select one arguments from two. Here I choose TRUE and FALSE approach:
So A is shaped like

(p: (SND p) (...) (...))

Besides, S and S’ must be TRUE and FALSE.
Now use the two constraints we learned from ((k+1) A B) and (1 A B), we can deduce that A is

(p: (SND p) (f (FST p), S) (x, S))

PRE
= n:f:x:
  n (p: (SND p) (f (FST p), S) (x, S))
    (x, FALSE)
    TRUE
= n:f:x:
  n (p: (SND p) (PAIR (f (FST p)) TRUE) (PAIR x TRUE))
    (PAIR x FALSE)
    TRUE

Bonus solution

After you finished the level SUB, do not forget to come back and write down

n:SUB n 1

This should beat other solutions in both reduction steps and function usage.

Thanks to morusleaf for his great guide, all credit to his effort. you can also read the original guide from Steam Community. enjoy the game.