Prev: New Primitive Programming Language - Is it Turing Complete?
Next: The size of proper classes?
From: Tegiri Nenashi on 13 Dec 2009 17:56
On Dec 11, 4:44 pm, Marshall <marshall.spi...(a)gmail.com> wrote:
> On Dec 11, 11:15 am, Tegiri Nenashi <tegirinena...(a)gmail.com> wrote:
>
> > On Dec 11, 9:51 am, Marshall <marshall.spi...(a)gmail.com> wrote:
>
> > > On Dec 2, 7:00 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> > > > ...your hand at Agda!
>
> > > Wow.
>
> > Unfortunately, it is based upon flawed assumption:
> > "Predicates are dependent types"
>
> Can you elaborate? The theory isn't sufficiently powerful
> for your tastes, because of self-imposed limitations?
> Or do you instead see some flaw?

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.3325

Type theory as a foundation for database theory? This is quite
ambitious statement unsupported by anything I read in the paper. Much
ado about constraints, but it is really an algebra that gives us a
tool to solve equations. BTW the constraint "No person teaches the
class he attends to" is expressed as:

T /^ A = [].

where
- "T" is relation "person p teaches class c"
- "A" is relation "person p attends class c"
- "/^" is set intersection join, that is natural join of two relation
projected to the set of their distinguished attributes
- "[]" is empty relation with empty set of attributes (aka DUM).

First  |  Prev  | 
Pages: 1 2 3
Prev: New Primitive Programming Language - Is it Turing Complete?
Next: The size of proper classes?