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

Quote from dandl on May 31, 2020, 6:51 amThe 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.

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 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.