[Prev][Next][Index][Thread]

Notations for abstraction and product formation



Date: Thu, 5 Mar 92 10:57:38 EST

According to the information received in reply to my earlier query about
type-labeled lambda-abstraction, abstraction terms of the form
lambda x:X.Y were, in fact, introduced by de Bruijn.  (Jon Seldin
gets the palm here --- he located this form of abstraction in an
old technical report written by de Bruijn, and nobody has come up with
an earlier reference.  I also had helpful correspondence about the
question with Mike Beeson, Roger Hindley, and Phil Scott.)

Does anybody know where the related notation for products, Pi x:X.Y,
originated?  Martin-Lof has been using (essentially) this notation
for a long time in his work on constructive type theory, but perhaps
it comes from AUTOMATH, too.

Garrel Pottinger
garrel@oracorp.com