Home » forums » LtU Forum

Computer Science/Mathematical Notations

I was just reading this paper from the home page

http://pauillac.inria.fr/~fpottier/slides/fpottier-2007-05-linear-bestiary.pdf

and realized I can't remember the meaning of many of the symbols after not using them for some time. Is there a reference somewhere that explains these symbols. I'm finding it hard to locate one.

Thank you.

By Patrick Dewane at 2009-08-24 16:05 | LtU Forum | previous forum topic | next forum topic | other blogs | 5635 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

wikipedia

In picking up this notation for the first time I found wikipedia's Calculus of Constructions very helpful. And if you really want to get back to basics then you can start with Lambda Calculus.

By andrew johnson at Sun, 2009-08-30 12:24 | login or register to post comments

Somewhat underwhelmed...

I'm somewhat underwhelmed by the section on Terms...

Terms

A term in the calculus of constructions is constructed using the following rules:

    * T is a term (also called Type)
    * P is a term (also called Prop, the type of all propositions)
    * If A and B are terms, then so are
          o \mathbf{(} A B )
          o (\mathbf{\lambda}x:A . B)
          o (\forall x:A . B)

The calculus of constructions has four object types:

   1. proofs, which are terms whose types are propositions
   2. propositions, which are also known as small types
   3. predicates, which are functions that return propositions
   4. large types, which are the types of predicates. (P is an example of a large type)
   5. T itself, which is the type of large types.

It's a bit like a bullet list of non-sequiturs. Anything with a bit more meat on the bones? Or even better, can anyone edit the Wikipedia entry and add that meat?

By John Carter at Mon, 2009-08-31 23:58 | login or register to post comments

thanks!

Thanks Andrew, CoC is exactly what I'm looking for.

By Patrick Dewane at Mon, 2009-08-31 17:10 | login or register to post comments