[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