How do you convert to lambda syntax?

Question

Part of a question I'm trying to understand involves this:

twice (twice) f x , where twice == lambda f x . f (f x)

I'm trying to understand how to make that substitution, and what it means.

My understanding is that (lambda x y . x + y) 2 3 == 2 + 3 == 5. I don't understand what twice (twice) means, or f ( f x ).

Answer 1

Two ways of looking at this.

Mechanical application of beta-reduction

You can solve this mechanically just by expanding any subterm of the form twice F X - with this term you will eventually eliminate all the occurences of twice, although you need to take care that you really understand the syntax tree of the lambda calculus to avoid mistakes.

twice takes two arguments, so your expression twice (twice) f x is the redex twice (twice) f applied to x. (A redex is a subterm that you can reduce independently of the rest of the term).

Expand the definition of twice in the redex: twice (twice) f x -> twice (twice f).

Substitute this into the original term to get twice (twice f) x, which is another redex we can expand twice in to get twice f (twice f x) (take care with the brackets in this step).

We have two twice redexes we can expand here, expanding the one inside the brackets is slightly simpler, giving twice f (f (f x)), which can again be expanded to give f (f (f (f x))).

Semantics of twice via abstraction

You can see what's going on at a more intuitive level by appealing to a higher-order combinator, the "○" infix combinator for function composition:

f ○ g = lambda x. f (g x)

It's easy to verify that twice f x and (f ○ f) x both expand to the same normal form, i.e., f (f x), so by extensionality, we have

twice f = f ○ f

Using this, we can expand very straightforwardly, first eliminating twice in favour of the composition combinator:

twice (twice) f x
= (twice ○ twice)  f x
= (twice (twice f)) x         /* expand out '○' */
= (twice (f ○ f)) x
= ((f ○ f) ○ (f ○ f)) x

and then expanding out '○':

= (f ○ f) ((f ○ f) x)
= (f ○ f) (f (f x))
= (f (f (f (f x))))

That's more expansion steps, because we first expand to terms containing the '○' operator, and then expand these operators out, but the steps are simpler, more intuitive ones, where you are less likely to misunderstand what you are doing. The '○' is widely used, standard operator in Haskell and is well worth getting used to.