Quote from dandl on May 31, 2020, 6:51 am

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 = S₁ U S₂ U S₃ … 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.