I have a question that I can't solve:

Given the simply typed lambda-calculus with call-by-value evaluation and the regular inference rules for abstraction, application and variables. If I just add the Unit type with the constant *:Unit, is the following true?

If t -> t' and t':T, then t:T

I suspect the answer is no, but I can't come up with a counterexample.

  • 1
    $\begingroup$ Hi, this site is for research-level questions only. Your question is suitable for cs.stackexchange.com. Please remove it from here and ask there. I promise to answer it there (you're looking for a standard theorem). $\endgroup$ – Andrej Bauer Oct 17 at 7:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.