The Forum for Discussion about The Third Manifesto and Related Matters

You need to log in to create posts and topics.

Formal definitions for Relation Constant, Transitive Closure, Extended Transitive Closure

The following are updated and corrected versions of definitions posted earlier, plus Extended TC. There are formatting issues, for which I apologise, but I find this editor very difficult to drive.

New Value as Relational Constant

This is the formalisation of a relational constant or ‘relcon’, and relies on a previously defined function. Separate formalisations are provided for monadic and dyadic functions. Extending them to n-adic functions is left as an exercise.

Monadic

Given a function f with the type signature Tx->Ty, the relcon S is defined as follows.

Hs = { <X,Tx>, <Y,Ty> }
Bs = { ts : exists vx ∈ Tx exists vy ∈ Ty 
  (ts = {<X,Tx,vx>, <Y,Ty,vy>} and f(Vx) = Vy)}

Dyadic

Given a function f with the type signature Tx->Ty->Tz, the relcon S is defined as follows.

Hs = { <X,Tx>, <Y,Ty>, <Z,Tz>}
Bs = { ts : exists vx ∈ Tx exists vy ∈ Ty exists vz ∈ Tz
  (ts = {<X,Tx,vx>, <Y,Ty,vy, <Z,Tz,vz>} and f(Vx,Vy) = Vz)}

For the relcon PLUS in App-A, types Tx, Ty and Tz are all INTEGER, and the function f is the scalar operator "+".

Note that a ‘relcon’ can be used as one argument to a join. Operations sometimes known as WHERE, EXTEND, UPDATE and DELETE are shorthands that may include such a combination.

Transitive Closure

This formalisation defines a recurrence relation consisting of a starting value and the elements of a sequence. The transitive closure is the union of that sequence, which can be shown to reach a fix-point termination. The starting point (‘seed’) represents known edges in a directed graph; the end alue is all the possible paths through the graph.

Given a set S of tuples with the heading {<X,T>,<Y,T>} for some type T, the successor relation S’ is defined as follows.

Hs’ = Hs
Bs’ = { ts’ : ts’ ∈ Bs or
(exists v1 ∈ T exists v2 ∈ T exists v3 ∈ T exists v4 ∈ T
exists ts1 ∈ Bs (ts1 = {<A,T,v1>, <B,T,v2>})
exists ts2 ∈ Bs (ts2 = {<A,T,v2>, <B,T,v3>})
ts’ = {<A,T,v1>, <B,T,v3>} )) }

The transitive closure T is then defined as

T = S1 U S2 U S3 … S

Note that this is a linear recurrence, not a predicate. Transitive closure cannot be defined by first order predicate logic.

Note that the operation sometimes known as TCLOSE corresponds to this definition.

Extended Transitive Closure

This formalisation defines a recurrence relation consisting of a starting value and the elements of a sequence. The transitive closure is the union of that sequence, which can be shown to reach a fix-point termination. The starting point (‘seed’) represents known edges in a directed graph; the end value is all the possible paths through the graph.

In this case each tuple is associated with a value, and this definition relies on some previously defined function f that takes values of that type as its argument.

Given a set S of tuples with the heading {<A,T>,<B,T>,<C,Tv>} for some types T and Tv, and a dyadic function f with the type signature Tv->Tv->Tv, the successor relation S’ is defined as follows.

Hs’ = Hs
Bs’ = { ts’ : ts’ ∈ Bs or
  (exists v1 ∈ T exists v2 ∈ T exists v3 ∈ T exists v4 ∈ T 
   exists w1 ∈ Tv exists w2 ∈ Tv
   exists ts1 ∈ Bs (ts1 = {<A,T,v1>, <B,T,v2>, <C,Tv,w1>})
   exists ts2 ∈ Bs (ts2 = {<A,T,v2>, <B,T,v3>, <C,Tv,w2>}) 
   ts’ = {<A,T,v1>, <B,T,v3>, <C,Tv,f(w1,w2)} )) }

The transitive closure T is then defined as

T = S1 U S2 U S3 … S∞

Note that this is a linear recurrence, not a predicate. Transitive closure cannot be defined by first order predicate logic.

Note that the function enables a cost to be calculated for each path. Generalised Transitive Closure as defined by D&D (RM VSS 5) requires an additional step of aggregation.

Andl - A New Database Language - andl.org