2008年10月8日星期三

varias logic system

what is the relation of following logic/caculus system?

  1. system T
  2. PCF
  3. LCF
  4. system F
  5. system Fw

some of them is discussed in "Practical Foundations for ProgrammingLanguages".

the most basic one is untyped lamda calculus, which suffer form paradoxes that refer to a set himself.
to avoid such paradoxes, Simply typed lambda calculus is invented, by incorporate -> as the only type combinator.

system T extend Simply typed lambda calculus with producat, coproducts and natual number.

PCF extend Simply typed lambda calculus with recursion.

above two one can still be called simply one, because they can still be expressed within the reach of ->.

more power full one like system F , which include polymorphic, and LF that include dependent type, are not simply one any more, because they are beyond the -> .

没有评论: