Can we form a finite set of well typed calculus of construction terms such that any closed term can be built up from them (plus the type of large types) using only application?

I conjecture that the following four combinators suffice:

  • P : T
  • ∏ = λx:P. λy:(x→P). (∀a:x. ya)
  • S = λx:P. λy:P. λz:P. (λa:(z→y→x). λb:(z→y). λc:z. ac(bc))
  • K = λx:P. λy:P. (λa:x. λb:y. x)

(You would also need to have the above three combinators with P replaced by T, I think.)

For example, the type of m→n is ∏m(K P m n) (for closed terms m:P and n:P).



Your Answer

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