4 ms·

> What exactly have you tried to do there? Isn't a schema already a model? What properties did you want your model to have? Yes, a schema is a data-model, and

> What exactly have you tried to do there? Isn't a schema already a model? What properties did you want your model to have? Yes, a schema is a data-model, and a database can tell you whether the row you are trying to insert satisfies the constraints, but it can't tell you whether an instantiation of the database exists, nor can it tell you how to construct it. There are 2 issues here, first proving that an instantiation exists; and second proving that there's a sequence of insertions that satisfy the constraints. Notice that some tables can have non sat constraints. This becomes significantly harder when you are dealing with recursive definitions, cycles in the dependencies, foreign keys that refer different tables across the same constrained columns, type compatibility, and on and on In other words, the space of all databases described by a schema may not even be constructible :upside_down:

auggierose 3y ago
Ok, I understand. So first you want to see your schema as a property on a database (which is just a bunch of tables with data, I guess), and see if there is actually any such database, or if the property is always false. Second, assuming that there are any such databases: Given certain commands which operate on databases, is there any sequence of commands which transform the empty database into a database such that the schema property holds for it? Actually, you probably would want the property to be true for every intermediate step as well, right? Sounds interesting! Although in practice, solving this is probably not that important, because if you cannot come up with some examples of constructing databases for your schema and application, then the schema is the wrong one pretty much by definition.
- PartiallyTyped 3y ago
  You needn’t think of databases as tables and data, you may think of them as trees of structs, ie an object relational model and show satisfiability of the model by constructing a tree of dependencies. You can do it incrementally for parts of the model, but that doesn’t guarantee that long range dependencies are satisfiable. Yes, you then need to show that it is incrementally constructible, which is a different can of worms… the tree view above isn’t actually fully correct because you duplicate entries mapping to the same object. Because of this duplication, the tree may refer to an object that can only be inserted later. Oh and the encoding must be able to accommodate arbitrary length arrays and arbitrary objects … which makes usage of SMT solvers difficult to say the least. While I agree that for the average company this isn’t useful, and the average engineer won’t shoot their feet on purpose, what I am doing needs to accommodate all those scenarios because I have no guarantees of sanity.
  - auggierose 3y ago
    Now I am interested in what exactly your use case is :-) Maybe you would want to model this first in a general purpose interactive prover such as Isabelle, and proceed from there. But in the end you seem to be looking for a push-button algorithm for proving the consistency of a particular logic, and I can tell you, that's probably not gonna end well.
    - PartiallyTyped 3y ago
      I can't say much more unfortunately, not yet at least. I have semi-sketched the idea in Dafny instead of Isabelle. Direct encoding of arrays makes it difficult, but I am thinking iterative deepening might just work. I am working on a Z3 approach for this, and I am crossing my fingers. If Z3 doesn't work, I will try emitting Dafny code instead and hooking up to the compiler.

auggierose 3y ago

Ok, I understand. So first you want to see your schema as a property on a database (which is just a bunch of tables with data, I guess), and see if there is actually any such database, or if the property is always false. Second, assuming that there are any such databases: Given certain commands which operate on databases, is there any sequence of commands which transform the empty database into a database such that the schema property holds for it? Actually, you probably would want the property to be true for every intermediate step as well, right? Sounds interesting! Although in practice, solving this is probably not that important, because if you cannot come up with some examples of constructing databases for your schema and application, then the schema is the wrong one pretty much by definition.

PartiallyTyped 3y ago
You needn’t think of databases as tables and data, you may think of them as trees of structs, ie an object relational model and show satisfiability of the model by constructing a tree of dependencies. You can do it incrementally for parts of the model, but that doesn’t guarantee that long range dependencies are satisfiable. Yes, you then need to show that it is incrementally constructible, which is a different can of worms… the tree view above isn’t actually fully correct because you duplicate entries mapping to the same object. Because of this duplication, the tree may refer to an object that can only be inserted later. Oh and the encoding must be able to accommodate arbitrary length arrays and arbitrary objects … which makes usage of SMT solvers difficult to say the least. While I agree that for the average company this isn’t useful, and the average engineer won’t shoot their feet on purpose, what I am doing needs to accommodate all those scenarios because I have no guarantees of sanity.
- auggierose 3y ago
  Now I am interested in what exactly your use case is :-) Maybe you would want to model this first in a general purpose interactive prover such as Isabelle, and proceed from there. But in the end you seem to be looking for a push-button algorithm for proving the consistency of a particular logic, and I can tell you, that's probably not gonna end well.
  - PartiallyTyped 3y ago
    I can't say much more unfortunately, not yet at least. I have semi-sketched the idea in Dafny instead of Isabelle. Direct encoding of arrays makes it difficult, but I am thinking iterative deepening might just work. I am working on a Z3 approach for this, and I am crossing my fingers. If Z3 doesn't work, I will try emitting Dafny code instead and hooking up to the compiler.