Home » forums » LtU Forum

Question from Pierce's Types and Programming Languages

On page 56 at the top of the page he has the reduction:

( λx . x ( λx . x ) )( u r ) evaluates to u r ( λx . x )

My question is:

I see how the lhs can be written as: (id(id))(ur) which is then (id)(ur). What I don't get is: (id)(ur) = (ur)(id). Is the point that the identity term is commutative in this context? Is this the same idea as the composition operation between functions in that the composition of two functions is generally not commutative, but the identity function is always commutative?

By markt at 2008-01-26 13:21 | LtU Forum | previous forum topic | next forum topic | other blogs | 4591 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I see how the lhs can be

I see how the lhs can be written as: (id(id))(ur)

Actually it can't - ( λx . x ( λx . x ) ) is "apply parameter to id".

By Philippa Cowderoy at Sat, 2008-01-26 13:29 | login or register to post comments

Oh I see, it's like this:

Oh I see, it's like this:

( λx . x t )( v ) evaluates to v t

where t = λx.x and v = ur

Thanks

By markt at Sun, 2008-01-27 14:47 | login or register to post comments