Strip `FALSE` prefix from Boolean list using the y-combinator? Stumped

Question

Given a list, e.g. (f: f FALSE (g: g FALSE (h: h TRUE FALSE))), write an operator that removes all leading FALSEs and returns only the tail that starts with TRUE. For this example the operator should return just (h: h TRUE FALSE).

This is an exercise, in fact a level, in this game called "functional" that I've become obsessed with. In the previous level we were required to generalized \Omega into the y-combinator so I imagine that this level requires the y-combinator in order to handle a FALSE prefix of arbitrary length.

I'm able to handle a single FALSE prefix with (b: c: IF b (f: f b c) c). Imagining that operator as f I'm guessing the answer should look something like (b: c: IF b (f: f b c) (Y c)). The game is rejecting that answer complaining about "no reduction (grew too big)".

I'm clearly baffled by the y-combinator. Can someone show me how to use it correctly?

Also, what is this crazy syntax the game is using? I don't see it used anywhere else.

As requested, a link to functional's page on Steam is here. I also recently uncovered a link the projects page on github here.

Answer 1

Try this: Y(f: x: (FST x) x (f(SND x))).

By using Y-combinator, it returns the whole list (x) if the head (FST x) is TRUE and recursively calls itself taking the tail (SND x) as an argument otherwise.

Answer 2

I spent a while stuck on this question. Let me explain why an incorrect answer doesn't work, then give the solution.

I first tried to solve this problem "imperatively." I tried to sketch a solution that said, "if the first element is TRUE, use the list (and we're done), otherwise call itself with skip-the-first-element." This incorrect solution looks like

t: IF (FST t) t (Y (x: SND t))

Look what happens with the test cases:

Case 1 (list=FALSE FALSE TRUE TRUE FALSE): ... failure.

Case 2 (list=TRUE FALSE): The first element in the list is TRUE, so the IF statement returns the entire list. Success.

Case 3 (list=FALSE TRUE): The IF statement fails, this reduces to

(f: f (PAIR FALSE (PAIR TRUE FALSE))) t: IF (FST t) t (Y (x: SND t))
...
Y (x: SND (PAIR FALSE (PAIR TRUE FALSE)))
...
SND (PAIR FALSE (PAIR TRUE FALSE))
...
PAIR TRUE FALSE # single element list containing TRUE

Case 3 succeeds, but only by accident. The Y combinator isn't doing anything helpful.

---

Let me copy some text from the problem:

Suppose you want to write a function that receives two arguments and applies itself to both arguments in inverted order. You can write: F = Y (f: x:y: f y x).

Pondering the above example and the case 3 above finally made it clear how to use the Y Combinator. You need to start with the Y Combinator, and use a function that you want to apply to itself. This function will have a list argument, but will more or less follow the same logic as I tried to implement the first time. Correct solution:

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

This solution says:

Apply this function to itself. If the first element in the list is TRUE, return the entire list and we're done (the IF (FST x) x part).

Otherwise, apply itself on the skip-the-first-element list (the f (SND x) part).