Question to Fixpoint Combinator

Moderator: Type Systems of Programming Languages

Stao
Mausschubser
Mausschubser
Beiträge: 60
Registriert: 12. Feb 2008 20:54

Question to Fixpoint Combinator

Beitrag von Stao »

In the solution of A4 / Task 2 :

Possibility 1 states:
...
-> (\n. (\y. (\x. myfun (\y. x x y)) (\x. myfun (\y. x x y)) y) (n+1))
-> (\n. Z myfun (n+1))

in my opinion it should be:

-> (\n. (\y. (\x. myfun (\y. x x y)) (\x. myfun (\y. x x y)) y) (n+1))
-> (\n. (\y. (Z myfun) y) (n+1))

where is \y ... y ?

the same is in Possibility 2:

-> myfun (\y. (\x. myfun (\y. x x y)) (\x. myfun (\y. x x y)) y)
-> myfun (Z myfun)

instead of:

-> myfun (\y. (\x. myfun (\y. x x y)) (\x. myfun (\y. x x y)) y)
-> myfun (\y. (Z myfun)y)

where is my mistake?

erdweg
Moderator
Moderator
Beiträge: 60
Registriert: 28. Mär 2013 10:08

Re: Question to Fixpoint Combinator

Beitrag von erdweg »

You are right, there is an intermediate step missing, I added it to the solution.

You can reduce

Code: Alles auswählen

(\y. f y)
to by what is called eta-reduction. This reduction makes sense because the lambda is only forwarding the argument anyway; you might as well call f directly. (Note that this may lead to the evaluation of , which was previously covered by the lambda.)

Hope this helps,
Sebastian

Stao
Mausschubser
Mausschubser
Beiträge: 60
Registriert: 12. Feb 2008 20:54

Re: Question to Fixpoint Combinator

Beitrag von Stao »

yes :) thanks

Antworten

Zurück zu „Type Systems of Programming Languages“