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 signatureTx->Ty
, the relconS
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 signatureTx->Ty->Tz
, the relconS
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 typeT
, the successor relationS’
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 asT = 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 typesT
andTv
, and a dyadic functionf
with the type signatureTv->Tv->Tv
, the successor relationS’
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 asT = 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 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.