Wiki needs documentation on "DP" tab for "Decide Equation-in-ctx" and "Sat"

[Skyfold]

After running a file all instance, schema and typeside have a "DP" tab with a button for "Decide Equation-in-ctx" and Input box. Would it be possible to elaborate on what this is and the syntax the input expects in the wiki?

The same goes for the Sat tab for each instance. I'm guessing its for setting the type (entity?) all to one value. Not sure about the syntax here either.

Any information would be appreciated.

[wisnesky]

Most of the panels in the viewer are actually intended to help debugging, so I've been remiss in documenting them. But I will do so now.

On Jul 12, 2019, at 7:04 AM, Pfalzgraf Martin notifications@github.com wrote:

After running a file all instance, schema and typeside have a "DP" tab with a button for "Decide Equation-in-ctx" and Input box. Would it be possible to elaborate on what this is and the syntax the input expects in the wiki?

The same goes for the Sat tab for each instance. I'm guessing its for setting the type (entity?) all to one value. Not sure about the syntax here either.

Any information would be appreciated.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[wisnesky]

I added a page to the wiki: https://github.com/CategoricalData/CQL/wiki/what-all-the-Viewer-panes-are . Do please let me know if there's any missing info.

[Skyfold]

Would it be possible to add some examples of input syntax?

For example: if you load up the Tutorial example and go to schema S you can type these valid equations which come from their path_equations:

Employee.manager.worksIn = Employee.worksIn

is written as:

forall x:Employee. worksIn(manager(x)) = worksIn(x)

Department.secretary.worksIn = Department

is written as:

forall x:Department. worksIn(secretary(x)) = x

But you can also ask questions about the schema like, "is the manager of the secretary of the department that each employee works in that employee?" (Which is clearly false in this case)

forall x:Employee. manager(secretary(worksIn(x))) = x

Note: you can add extra variables like so:

forall d:Department, e:Employee. secretary(d) = e

Though I'm not sure how to add Existential quantifiers.

Note: "A path equation such as X.p.q = X.l should be input as forall x:X. p(q(x)) = l(x). -- Acyclic" Should be "A path equation such as X.p.q = X.l should be input as forall x:X. q(p(x)) = l(x). -- Acyclic". The p and q should be swapped. I noticed this by pattern matching X.p.q = X.l with Employee.manager.worksIn = Employee.worksIn then substituting the terms into forall x:X. p(q(x)) = l(x). Of course this does not make sense given that worksIn returns a Department and manager takes an Employee, thus you get "Cannot infer a well-sorted term for manager(worksIn(x)).".

[Skyfold]

Question: When you say: "A path equation such as X.p.q = X.l should be input as forall x:X. p(q(x)) = l(x). -- Acyclic: Returns yes or no if the underlying graph of the schema is acyclic.", does that mean any schema with a path_equations of the form X.p.q = X.l is acyclic regardless of how many foreign_keys there are? Or are you saying that any permutation of forall x:X. p(q(x)) = l(x) (that type checks) must be true for a schema to be acyclic?

[wisnesky]

I think you are noticing that in CQL, the type of "." is (A->B) * (B->C) -> (A->C), i.e., it is not Haskell's dot, but left-to-right composition.

There can't be any existential quantifiers or implications in any of the DP inputs - they are (intended to be) restricted to equations of exactly the form of their corresponding kinds, typeside, schema, and instance.

On Jul 13, 2019, at 11:22 AM, Pfalzgraf Martin notifications@github.com wrote:

Would it be possible to add some examples of input syntax?

For example: if you load up the Tutorial example and go to schema S you can type these valid equations which come from their path_equations:

Employee.manager.worksIn = Employee.worksIn

is written as:

forall x:Employee. worksIn(manager(x)) = worksIn(x)

Department.secretary.worksIn = Department

is written as:

forall x:Department. worksIn(secretary(x)) = x

But you can also ask questions about the schema like, "is the manager of the secretary of the department that each employee works in that employee?" (Which is clearly false in this case)

forall x:Employee. manager(secretary(worksIn(x))) = x

Note: you can add extra variables like so:

forall d:Department, e:Employee. secretary(d) = e

Though I'm not sure how to add Existential quantifiers.

Note: "A path equation such as X.p.q = X.l should be input as forall x:X. p(q(x)) = l(x). -- Acyclic" Should be "A path equation such as X.p.q = X.l should be input as forall x:X. q(p(x)) = l(x). -- Acyclic". The p and q should be swapped. I noticed this by pattern matching X.p.q = X.l with Employee.manager.worksIn = Employee.worksIn then substituting the terms into forall x:X. p(q(x)) = l(x). Of course this does not make sense given that worksIn returns a Department and manager takes an Employee, thus you get "Cannot infer a well-sorted term for manager(worksIn(x)).".

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[wisnesky]

The underlying graph of a schema consists of the entities and foreign keys, considered as a directed multi-graph, ignoring the equations altogether.

There is another question you can ask: is the category presented by schema finite, which takes the equations into account. That is not implemented, but is a good first issue with an open ticket. In general, because of the automated theorem prover, there's no need for any CQL schemas to be finite.

On Jul 13, 2019, at 11:27 AM, Pfalzgraf Martin notifications@github.com wrote:

Question: When you say: "A path equation such as X.p.q = X.l should be input as forall x:X. p(q(x)) = l(x). -- Acyclic: Returns yes or no if the underlying graph of the schema is acyclic.", does that mean any schema with a path_equations of the form X.p.q = X.l is acyclic regardless of how many foreign_keys there are? Or are you saying that any permutation of forall x:X. p(q(x)) = l(x) (that type checks) must be true for a schema to be acyclic?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.