## The Forum for Discussion about The Third Manifesto and Related Matters

Forum breadcrumbs - You are here:
Please or Register 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.

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)}```

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