Formalisation of Transitive Closure

#1 · May 30, 2020, 3:44 am

Given a set S of tuples with the heading Hs=<X,T>,<Y,T> and body Bs representing edges in a directed graph the relation S' is defined as follows.

Hs' = Hs
Bs' = { ts' | ts' ∈ Bs or ts'<any,X> ∈ Bs or ts'<Y,any> ∈ Bs }

The transitive closure T is then defined as

T = S' U S'' U S''' …

This series has a fix-point termination, which represents the primitive operation that prevents this from being expressed in terms of other operators.

It may be possible to extend this idea to generalised TC. It is still less powerful than while or recursion.

Andl - A New Database Language - andl.org

#2 · May 30, 2020, 7:03 am

.

#3 · May 30, 2020, 8:33 am

Quote from dandl on May 30, 2020, 8:33 am
Quote from AntC on May 30, 2020, 7:03 am
Quote from dandl on May 30, 2020, 3:44 am

Given a set S of tuples with the heading Hs=<X,T>,<Y,T> and body Bs representing edges in a directed graph the relation S' is defined as follows.
Hs' = Hs
Bs' = { ts' | ts' ∈ Bs or ts'<any,X> ∈ Bs or ts'<Y,any> ∈ Bs }
The transitive closure T is then defined as
T = S' U S'' U S''' …
This series has a fix-point termination, which represents the primitive operation that prevents this from being expressed in terms of other operators.

It may be possible to extend this idea to generalised TC. It is still less powerful than while or recursion.
Let s be TCLOSE r. It is required that there exist some type T and distinct attributes A, B such that Hr = { <A,T>, <B,T> }.
Hs = Hr.
Bs = { ts : ts ∈ Br or (exists v1 exists v2 (v1 ∈ T and v2 ∈ T and ts = {<A,T,v1>, <B,T,v2>} and
exists ts1 exists ts2 exists v
( ts1 ∈ Bs and ts2 ∈ Bs and ts1 ≠ ts2 and v ∈ T and ts1 = {<A,T,v1>,<B,T,v>} and ts2 = {<A,T,v>,<B,T,v2>} ) ) ) }.

(I might have mis-matched my bracketing there.)

I don't think it's hard to follow the style of Appendix A. I don't understand why you can't even keep to its typographical conventions. What does ts'<any,X> mean?
I dislike the App-A style for various reasons, but I agree: their notation is preferable for dealing with <any>. I'll consider reposting it.

I'm a little unsure of my algebraic ground, but as far as I understand it: this definition is 'linear recursive' in that Bs's definition includes ts1 ∈ Bs and ts2 ∈ Bs self-reference. This keeps it within first-order; whereas Generalised Transitive Closure requires second-order.

But no, here I disagree. I do not believe this is linear recursive, or that it is first order, or that it is well-formed set-builder notation, or that it is correct.

this is not in the form of a linear recursion (but what I wrote was).

It's not first order recursive, or FOPL (which did you mean?).

You can't 'bootstrap' in set-builder notation; even if you were allowed to refer back to the set you are building, the members you want are not there. You need a way to get multiple passes through the process, ending when there are no more members to add, and your formulation doesn't do that. I tried your approach first, but I found it doesn't work and I think it's doomed to failure.

You need to have a 'v2' occupying the A position or you don't get edge propagation.

I have no patience to figure out how this corresponds to Alice's while. In general I do not expect a formalism in one textbook to exactly mirror a different formalism in a different textbook. If Alice's while is second-order and strictly more general, then TCLOSE is less expressive; but keeping TCLOSE to first-order makes the algebra decidable. That is of value even if the algebra is embedded in a programming language that is Turing complete.

This has nothing to do with Alice. This is a formulation of TCLOSE based on evaluating a series (a linear recursion, if you like) that is guaranteed to terminate, and which you have not rebutted. The path explosion first phase of GTC should yield to the same technique, in combination with a function relation (or 'relcon' if you prefer) from the previous post. The second phase needs aggregation, which I have not yet addressed. I expect it to need second order logic.

The while in Alice is simply the fixed point recursion from CTE in SQL. Baby steps, but ultimately I hope a query language as powerful as SQL. We're not there yet, by a long chalk.

Quote from AntC on May 30, 2020, 7:03 am
Quote from dandl on May 30, 2020, 3:44 am

Given a set S of tuples with the heading Hs=<X,T>,<Y,T> and body Bs representing edges in a directed graph the relation S' is defined as follows.
Hs' = Hs
Bs' = { ts' | ts' ∈ Bs or ts'<any,X> ∈ Bs or ts'<Y,any> ∈ Bs }
The transitive closure T is then defined as
T = S' U S'' U S''' …
This series has a fix-point termination, which represents the primitive operation that prevents this from being expressed in terms of other operators.

It may be possible to extend this idea to generalised TC. It is still less powerful than while or recursion.
Let s be TCLOSE r. It is required that there exist some type T and distinct attributes A, B such that Hr = { <A,T>, <B,T> }.
Hs = Hr.
Bs = { ts : ts ∈ Br or (exists v1 exists v2 (v1 ∈ T and v2 ∈ T and ts = {<A,T,v1>, <B,T,v2>} and
exists ts1 exists ts2 exists v
( ts1 ∈ Bs and ts2 ∈ Bs and ts1 ≠ ts2 and v ∈ T and ts1 = {<A,T,v1>,<B,T,v>} and ts2 = {<A,T,v>,<B,T,v2>} ) ) ) }.

(I might have mis-matched my bracketing there.)

I don't think it's hard to follow the style of Appendix A. I don't understand why you can't even keep to its typographical conventions. What does ts'<any,X> mean?

I dislike the App-A style for various reasons, but I agree: their notation is preferable for dealing with <any>. I'll consider reposting it.

I'm a little unsure of my algebraic ground, but as far as I understand it: this definition is 'linear recursive' in that Bs's definition includes ts1 ∈ Bs and ts2 ∈ Bs self-reference. This keeps it within first-order; whereas Generalised Transitive Closure requires second-order.

But no, here I disagree. I do not believe this is linear recursive, or that it is first order, or that it is well-formed set-builder notation, or that it is correct.

this is not in the form of a linear recursion (but what I wrote was).
It's not first order recursive, or FOPL (which did you mean?).
You can't 'bootstrap' in set-builder notation; even if you were allowed to refer back to the set you are building, the members you want are not there. You need a way to get multiple passes through the process, ending when there are no more members to add, and your formulation doesn't do that. I tried your approach first, but I found it doesn't work and I think it's doomed to failure.
You need to have a 'v2' occupying the A position or you don't get edge propagation.

I have no patience to figure out how this corresponds to Alice's while. In general I do not expect a formalism in one textbook to exactly mirror a different formalism in a different textbook. If Alice's while is second-order and strictly more general, then TCLOSE is less expressive; but keeping TCLOSE to first-order makes the algebra decidable. That is of value even if the algebra is embedded in a programming language that is Turing complete.

This has nothing to do with Alice. This is a formulation of TCLOSE based on evaluating a series (a linear recursion, if you like) that is guaranteed to terminate, and which you have not rebutted. The path explosion first phase of GTC should yield to the same technique, in combination with a function relation (or 'relcon' if you prefer) from the previous post. The second phase needs aggregation, which I have not yet addressed. I expect it to need second order logic.

The while in Alice is simply the fixed point recursion from CTE in SQL. Baby steps, but ultimately I hope a query language as powerful as SQL. We're not there yet, by a long chalk.

Andl - A New Database Language - andl.org

#4 · May 30, 2020, 8:48 am

.

#5 · May 30, 2020, 10:22 am

(Repost with style closer to App-A)

Given a set S of tuples with the heading <X,T>,<Y,T> representing edges in a directed graph the relation S' is defined as follows.

Hs’ = Hs
Bs’ = { ts’ : ts’ ∈ Bs or (exists v exists v1 exists v2 exists ts
  (v ∈ T and v1 ∈ T and v2 ∈ T and ts ∈ Bs and ts’ = {<A,T,v1>, <B,T,v2>}
  and (ts = {<A,T,v2>, <B,T,v>} or ts = {<A,T,v>, <B,T,v1>} ))) }

The transitive closure T is then defined as

T = S' U S'' U S''' …

This series is linear recursive with a fix-point termination, which represents the primitive operation that prevents this from being expressed in terms of other operators.

Andl - A New Database Language - andl.org

#6 · May 31, 2020, 12:29 am

.

#7 · May 31, 2020, 7:09 am

Quote from dandl on May 31, 2020, 7:09 am

Quote from AntC on May 31, 2020, 12:29 am

Quote from dandl on May 30, 2020, 8:33 am

Quote from AntC on May 30, 2020, 7:03 am

Quote from dandl on May 30, 2020, 3:44 am

Let s be TCLOSE r. It is required that there exist some type T and distinct attributes A, B such that Hr = { <A,T>, <B,T> }.
Hs = Hr.
Bs = { ts : ts ∈ Br or (exists v1 exists v2 (v1 ∈ T and v2 ∈ T and ts = {<A,T,v1>, <B,T,v2>} and
exists ts1 exists ts2 exists v
( ts1 ∈ Bs and ts2 ∈ Bs and ts1 ≠ ts2 and v ∈ T and ts1 = {<A,T,v1>,<B,T,v>} and ts2 = {<A,T,v>,<B,T,v2>} ) ) ) }.

(I might have mis-matched my bracketing there.)

I don't think it's hard to follow the style of Appendix A. I don't understand why you can't even keep to its typographical conventions. What does ts'<any,X> mean?

I'm a little unsure of my algebraic ground, but as far as I understand it: this definition is 'linear recursive' in that Bs's definition includes ts1 ∈ Bs and ts2 ∈ Bs self-reference. This keeps it within first-order; whereas Generalised Transitive Closure requires second-order.

But no, here I disagree. I do not believe this is linear recursive, or that it is first order, or that it is well-formed set-builder notation, or that it is correct.

You seem to be suffering from the delusion (common for you) that Appendix A FORMAL DEFINITIONS give algorithms or implementations. No.

Whatever gave you that idea? This definition is straight maths, modeled on those I found elsewhere on the Web.

Set-builded alone cannot do TC, but linear recursion can.

Linear recursion requires initial value, successor function, termination condition. Done.

this is not in the form of a linear recursion (but what I wrote was).

It's not first order recursive, or FOPL (which did you mean?).

It's obvious that all of the Set-builder in Appendix A is FOPL. Because Predicate Logic is the only thing allowed with Set-builder. This is not 'set comprehension' notation as used in programming languages -- because that notation is not Set-builder.

Correct, which is why I assume D&D did not attempt to formalise TCLOSE. They could see it was beyond FOPL/set-builder and they did not know another way.

You can't 'bootstrap' in set-builder notation; even if you were allowed to refer back to the set you are building, the members you want are not there. You need a way to get multiple passes through the process, ending when there are no more members to add, and your formulation doesn't do that. I tried your approach first, but I found it doesn't work and I think it's doomed to failure.

Again I did not give an algorithm; I gave a condition on membership. Just like all the Set-builder in Appendix A. Look for example at the definitions for <NOT>, <OR>. It's really difficult to follow what depths of misunderstanding you get into; then no wonder you exhaust people's patience in trying to unwind your persistent wrong-headedness.

That's not what I said: what you gave is invalid set-builder. For one thing, set-builder does not know the name of the thing it is building, so it cannot self-reference. For another, the things it references are static, they cannot be one thing at one point and something different at another point.

But that's to be expected: you can't define TCLOSE using FOPL, so obviously you can't do it in set-builder notation.

You need to have a 'v2' occupying the A position or you don't get edge propagation.

Strewth you really don't understand.

Where is the prohibition in Set-builder on a set's definition referring to itself? Citation needed; or did you just make it up out of thin air? Yes you can get into paradoxes of self-reference like that (not in this case); but that doesn't make it ill-formed. Just go and look for examples of self-reference, there's plenty. (There's also SO answers for how to get from self-referential Set-builder to non-self-r. I would have helped figure that out if you hadn't been so peremptory.)

No, I'm not going chasing for negative references. If you think that is valid use of set-builder notation, the onus is on you to find a competent authority that says so and gives an example.

No, I didn't find any such reference, but I'd be happy to see a link. Here's mine: https://math.stackexchange.com/questions/2391191/recursively-constructed-set-definition. What I wrote complies with the accepted answer.

Meanwhile, what I have provided is a valid definition without these difficulties. If you can find fault in it please do so. Otherwise, I move on. [I've done Extended TC, separate post.]

Quote from AntC on May 31, 2020, 12:29 am

Quote from dandl on May 30, 2020, 8:33 am

Quote from AntC on May 30, 2020, 7:03 am

Quote from dandl on May 30, 2020, 3:44 am

Let s be TCLOSE r. It is required that there exist some type T and distinct attributes A, B such that Hr = { <A,T>, <B,T> }.
Hs = Hr.
Bs = { ts : ts ∈ Br or (exists v1 exists v2 (v1 ∈ T and v2 ∈ T and ts = {<A,T,v1>, <B,T,v2>} and
exists ts1 exists ts2 exists v
( ts1 ∈ Bs and ts2 ∈ Bs and ts1 ≠ ts2 and v ∈ T and ts1 = {<A,T,v1>,<B,T,v>} and ts2 = {<A,T,v>,<B,T,v2>} ) ) ) }.

(I might have mis-matched my bracketing there.)

I don't think it's hard to follow the style of Appendix A. I don't understand why you can't even keep to its typographical conventions. What does ts'<any,X> mean?

I'm a little unsure of my algebraic ground, but as far as I understand it: this definition is 'linear recursive' in that Bs's definition includes ts1 ∈ Bs and ts2 ∈ Bs self-reference. This keeps it within first-order; whereas Generalised Transitive Closure requires second-order.

But no, here I disagree. I do not believe this is linear recursive, or that it is first order, or that it is well-formed set-builder notation, or that it is correct.

You seem to be suffering from the delusion (common for you) that Appendix A FORMAL DEFINITIONS give algorithms or implementations. No.

Whatever gave you that idea? This definition is straight maths, modeled on those I found elsewhere on the Web.

Set-builded alone cannot do TC, but linear recursion can.
Linear recursion requires initial value, successor function, termination condition. Done.

this is not in the form of a linear recursion (but what I wrote was).

It's not first order recursive, or FOPL (which did you mean?).

It's obvious that all of the Set-builder in Appendix A is FOPL. Because Predicate Logic is the only thing allowed with Set-builder. This is not 'set comprehension' notation as used in programming languages -- because that notation is not Set-builder.

Correct, which is why I assume D&D did not attempt to formalise TCLOSE. They could see it was beyond FOPL/set-builder and they did not know another way.

You can't 'bootstrap' in set-builder notation; even if you were allowed to refer back to the set you are building, the members you want are not there. You need a way to get multiple passes through the process, ending when there are no more members to add, and your formulation doesn't do that. I tried your approach first, but I found it doesn't work and I think it's doomed to failure.

Again I did not give an algorithm; I gave a condition on membership. Just like all the Set-builder in Appendix A. Look for example at the definitions for <NOT>, <OR>. It's really difficult to follow what depths of misunderstanding you get into; then no wonder you exhaust people's patience in trying to unwind your persistent wrong-headedness.

That's not what I said: what you gave is invalid set-builder. For one thing, set-builder does not know the name of the thing it is building, so it cannot self-reference. For another, the things it references are static, they cannot be one thing at one point and something different at another point.

But that's to be expected: you can't define TCLOSE using FOPL, so obviously you can't do it in set-builder notation.

You need to have a 'v2' occupying the A position or you don't get edge propagation.

Strewth you really don't understand.

Where is the prohibition in Set-builder on a set's definition referring to itself? Citation needed; or did you just make it up out of thin air? Yes you can get into paradoxes of self-reference like that (not in this case); but that doesn't make it ill-formed. Just go and look for examples of self-reference, there's plenty. (There's also SO answers for how to get from self-referential Set-builder to non-self-r. I would have helped figure that out if you hadn't been so peremptory.)

No, I'm not going chasing for negative references. If you think that is valid use of set-builder notation, the onus is on you to find a competent authority that says so and gives an example.

No, I didn't find any such reference, but I'd be happy to see a link. Here's mine: https://math.stackexchange.com/questions/2391191/recursively-constructed-set-definition. What I wrote complies with the accepted answer.

Meanwhile, what I have provided is a valid definition without these difficulties. If you can find fault in it please do so. Otherwise, I move on. [I've done Extended TC, separate post.]

Andl - A New Database Language - andl.org

#8 · May 31, 2020, 2:50 pm

Quote from dandl on May 31, 2020, 7:09 am

Quote from AntC on May 31, 2020, 12:29 am

[...]

You seem to be suffering from the delusion (common for you) that Appendix A FORMAL DEFINITIONS give algorithms or implementations. No.

Whatever gave you that idea? [...]

Gentlemen, please -- let's all endeavour to maintain a polite level of mutual respect and professional decorum. I appreciate that these are trying times and tempers are sometimes easily frayed, but that's reason to be more civil rather than less.

I'm the forum administrator and lead developer of Rel. Email me at dave@armchair.mb.ca with the Subject 'TTM Forum'. Download Rel from https://reldb.org

#9 · June 1, 2020, 3:56 am

Quote from Dave Voorhis on May 31, 2020, 2:50 pm

Quote from dandl on May 31, 2020, 7:09 am

Quote from AntC on May 31, 2020, 12:29 am

[...]

You seem to be suffering from the delusion (common for you) that Appendix A FORMAL DEFINITIONS give algorithms or implementations. No.

Whatever gave you that idea? [...]

Gentlemen, please -- let's all endeavour to maintain a polite level of mutual respect and professional decorum. I appreciate that these are trying times and tempers are sometimes easily frayed, but that's reason to be more civil rather than less.

Just to be clear, my intention is always to be courteous and objective. People make mistakes, and I try to work around those, but if an idea is wrong I reserve the right to say so. That translates into: hard on ideas, easy on people.

The phrase "whatever gave you that idea?" was intended to be read as "I don't see anything in what I wrote to lead to that conclusion, what did you think I said that would?" If it fell short, my apologies. I can rephrase.

In this thread, I have put forward formalisations; AntC has responded with his own. I think they're wrong and I shall say so, politely, but firmly, giving reasons. In my opinion that's the right thing to do, it's what I have been doing and intend to continue to do. You are very welcome to intervene if you see either of us over-stepping the mark, but as far as I can see I have not.

Andl - A New Database Language - andl.org

The Forum for Discussion about The Third Manifesto and Related Matters

Formalisation of Transitive Closure