4

This problem is coming from Exercise 3.3 in Bacon's A Philosophical Introduction to Higher-order Logics. I am trying to do my due-diligence here and not skip problems, but this one stuck out to me.

Exercise 3.3 Argue that the variables appearing in Y((λY.(λx.Yx))Z) cannot be assigned types that make it into a well-typed term.

The chapter endnotes include a hint to argue that Z has to be the same type as Y. I think I understand why if Z is the same type as Y, that the term is not well-typed: If Z and Y are of the same type (τ→σ) then the formula includes an instance of self-application (Y: τ→σ and (λY.(λx.Yx))Z : τ→σ), forbidden by STLC.

What I'm looking for help with is what exactly makes it the case that Z and Y are of the same type? Any hints or discussion would be greatly appreciated. Also, am I right about what makes it the case that if Z and Y are the same type, then the term is not well-typed? Thanks all!

Improve this question
1
  • Having a name collision of the outermost Y (free) along with the λY (bound) seems unnecessarily fiddly. [Of course in an exercise on free and bound variables its ok] But in an exercise on well typing it can trivially renamed so I dont get the point...
    – Rushi
    Commented Jan 2 at 16:47

1 Answer 1

Reset to default
2

upon further reading I think I've figured it out, and so I thought I'd my possible solution here.

Let's arbitrarily assign some types to X and Y in the formula Y((λY.(λx.Yx))Z) while intentionally not assigning Z a type.

Let's say that x : τ and Y : τ→σ. Then, we can note the following:

  • (λx.Yx) : τ→σ
  • (λY.(λx.Yx)) : (τ→σ)→(τ→σ)

therefore, for (λY.(λx.Yx))Z to be well-typed, it must be that Z is of type τ→σ. Therefore, Y and Z are of the same type. Hence, the reasoning from above should hold. If I've made any mistakes feel free to let me know :)

Improve this answer
2
  • 1
    This is correct. But note that the book's requirement that each variable has uniquely assigned type is not standard, in other sources you will more often find that the same variable may have different types in different contexts (like here we have one $Y$ free and one $Y$ bound in a lambda-abstraction)
    – Vladimir Lysikov
    Commented Jan 2 at 17:13
  • I noted this as well, the problem gives no reason to think that Y and λY are of the same type, but I merely took it for granted, otherwise Y could be assigned any type arbitarily such that the function is itself well-typed
    – C D
    Commented Jan 2 at 17:24

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .