Curry typing P-complete

To: types
Subject: Curry typing P-complete
From: John C. Mitchell <jcm@cs.stanford.edu>
Date: Thu, 4 Jul 91 15:49:45 EDT
Reply-To: John C. Mitchell <jcm@cs.stanford.edu>
Sender: meyer@theory.lcs.mit.edu

Date: Fri, 28 Jun 91 18:00:58 PDT

I was just reading Tiuryn's very nice survey article on 
type inference (1990 MFOCS proceedings). In this paper, he credits
J. Tyszkiewicz (even growing up in Wisconsin does not give
me any idea how to pronounce this one) with proving that
Curry type inference is P-complete. Since Tyszkiewicz has
already received his MS degree for this, I hope no one will suffer
if I point out that there is an essentially trivial proof
of this.

The following facts are well-known

1) An implicational formula A is intuitionistically valid iff
A is a Curry type of some lambda term.

2) If A, B are any implicational formulas, not containing propositional
symbol P, then A -> B -> P -> P is intuitionistically valid.

3) Unifiability of arbitrary implicational formulas is P-complete.

4) If A is a Curry type of term M, then there is some N reducible
to M with principal Curry type A. (This might be less well-known than
the others. It is in Hindley's 1969 paper, and actually quite easy
to prove if you use lambda terms instead of combinators.)

Corollary: Given term M, it is P-complete to decide whether
M has a Curry type.

Proof: For any implicational formulas A and B we can find a term
M with principal type  A -> B -> P -> P. It is easy to see that
\lambda x.Mxx is typable iff A and B are unifiable.

John Mitchell