We use cookies to ensure you have the best browsing experience on our website. Please read our cookie policy for more information about how we use cookies.
The transformation rule in Wikipedia is rather sloppy. For example,
T[λx.λy.E] ⇒ T[λx.T[λy.E]]
is, strictly speaking, incorrect, because λx.T[λy.E] is not a well-formed lambda-term. I am using rules from the textbook, Lectures on the Curry-Howard Isomorphisms by Sørensen and Urzyczyn, which however only produces an equivalent but smaller terms than the solutions.
Could you add the intended rules in the problem description to make rules clear?
Cookie support is required to access HackerRank
Seems like cookies are disabled on this browser, please enable them to open this website
Down With Abstractions
You are viewing a single comment's thread. Return to all comments →
The transformation rule in Wikipedia is rather sloppy. For example,
T[λx.λy.E] ⇒ T[λx.T[λy.E]]
is, strictly speaking, incorrect, because
λx.T[λy.E]
is not a well-formed lambda-term. I am using rules from the textbook, Lectures on the Curry-Howard Isomorphisms by Sørensen and Urzyczyn, which however only produces an equivalent but smaller terms than the solutions.Could you add the intended rules in the problem description to make rules clear?