Timeline for Lambda calculus typing

9 events

when toggle format	what	by	license	comment
May 20, 2015 at 18:44	comment	added	MJD		It could be. Depends on who you're talking to. Why is there no $b$ and $e$ for which $b=b\to e$?
May 20, 2015 at 18:00	comment	added	hunterge		Sorry, one more question. Is it okay to leave the last answer as a=b→(b→d), or is it important to substitute a=b→(b→d) into it?
May 20, 2015 at 17:45	comment	added	hunterge		Thanks, does that suffice as a 'proof'?
May 20, 2015 at 13:54	comment	added	MJD		Your conclusion is correct, but the reason isn't quite right. For example, suppose you found $b=p\to (q\to r)$ and also $b=(s\to t)\to u$. Does this fail? No, because you can unify these types by saying that $p=s\to t$ and $u=q\to r$. But in your example, say the type of $y$ is $b$ and the type of $yy$ is $e$. Then you need $b = b\to e,ドル and there is no such $b$. In this case the unification algorithm fails.
May 20, 2015 at 13:16	vote	accept	hunterge
May 20, 2015 at 13:16	comment	added	hunterge		That is brilliant, thank you very much! Does that mean that λx.λy.(x(yy)) is un-typable as it would mean the two y's would have different types which isn't possible?
May 19, 2015 at 17:51	history	edited	MJD	CC BY-SA 3.0	added 10 characters in body
S May 19, 2015 at 17:41	history	answered	MJD	CC BY-SA 3.0
S May 19, 2015 at 17:41	history	made wiki			Post Made Community Wiki by MJD