Beta reduction of Lambda Calculus

Question

I have the following lambda calculus:

1) λx . katze(x)(Garfield)

2) λP . λx . P(x)(tea)

3) λy . λx . likes(x, y)(Mia)

How do I reduce them with the Beta Reduction?

My solutions:

1) katze (Garfield)

2) tea

3) likes(Mia)

Answer 1

When performing beta reduction, you substitute the bound variable to the lambda function with the value supplied. The notation for that is [param := value] and you pick up the first variable that is given.

In the case λx . katze(x)(Garfield) -> katze (Garfield) the reduction is correct. We've substituted the x variable for Garfield and removed λx in the process leaving just the expression inside. Here are the steps that would be taken:

λx . katze(x)(Garfield)

= katze(x)[x := Garfield]

= katze(Garfield)

However, the other two are not correct. You are forgetting that you have a lambda function where the expression inside is another lambda function. Since you have a single input, you only have to reduce one function - the first one, leaving the other. You can think of it of peeling off the outer one and exposing the inner.

In the case of λP . λx . P(x)(tea) this can be better represented as (λP . (λx . P(x)))(tea) where now each lambda function is surrounded by brackets. Since we supply a single input tea, we only resolve the outer function with parameter P (leaving the brackets for some clarity):

(λP . (λx . P(x)))(tea)

= (λx . P(x))[P := tea]

= (λx . P(x))

= λx . tea(x)

Or without the brackets:

λP . λx . P(x)(tea)

= λx . P(x)[P := tea]

= λx . tea(x)

As for the final function, it still has the same problem that you are removing both functions, when only one input is given. The correct reduction steps are:

λy . λx . likes(x, y)(Mia)

= λx . likes(x, y)[y := Mia]

= λx . likes(x, Mia)