Type inference for datalog with complex type hierarchies

Patent metadata

Field	Value
Publication number	US-RE48405-E
Application number	US-201715494416-A
Country	US
Kind code	E1
Filing date	Apr 21, 2017
Priority date	Jul 15, 2010
Publication date	Jan 26, 2021
Grant date	Jan 26, 2021

Abstract

What is disclosed are a novel system and method for inferring types of database queries. In one embodiment a program and associated database schema that includes a type hierarchy is accessed. The program includes query operations to a database that contains relations described by a database schema. Types are inferred from definitions in the program by replacing each database relationship in the program by the types in the database schema. A new program is generated with the types that have been inferred with the new program only accessing unary relations in the database. In another embodiment, testing of each of the types that have been inferred is performed for type emptiness. In response to type emptiness being found for a type that have been inferred, a variety of different operations are performing including removing the type, providing a notification regarding the emptiness found for the type, and more.

First claim

What is claimed is:

1. A computer-implemented method comprising:
accessing a program with one or more queries to a database that contains relations described by at least one database schema; receiving the database schema and at least one entity type hierarchy for the database; and inferring a first type program from definitions in the program by replacing each use of a database relation in the program by its type in the database schema, and the type is at least portion of a second type program, wherein each of the first type program and the second type program is a derived program using type symbols without other extensional relation symbols, and each of the first type program and the second type program do not contain negation, wherein the first type program and the second type program uses monadic extensions; testing portion of the first type program that has been inferred for type emptiness and type inclusion; and providing at least one of error information and optimization information regarding the type emptiness and type inclusion being found for the type.

2. The computer-implemented method of claim 1 , further comprising:
in response to type emptiness being found for a portion of the first type program that has been inferred during determining of the testing portion of the first type program, performing at least one of:
removing the a type test;
providing a notification regarding the emptiness found for the portion of the first type program;
providing notification on combining queries by conjunction without creating empty parts in a combined query;
in response to an empty part of a query being a conjunction, finding a smallest set of query parts that has a conjunction that is empty; in response to a search for a smallest empty part of a database query that traverses all parts of the database query, pushing a conjunction of an approximation of the smallest empty part and a context on top of a stack of approximations of all contexts where the empty part is being used; and eliminating empty query parts to achieve virtual method resolution in an object-oriented query language.

3. The computer-implemented method of claim 1 , further comprising:
in response to type inclusion being found for a portion of the first type program that has been inferred during determining of the testing portion of the first type program, performing at least one of:
removing the a type test; and
providing a notification regarding the type inclusion being found for the portion type.

4. The computer-implemented method of claim 1 , further comprising:
testing the type program that has been inferred for whether a database query is contained in a given portion of the type program; and in response to the database query not being contained in the given portion, performing at least one of: removing a type test; and providing a notification regarding the database query not being contained in the given portion.

5. The computer-implemented method of claim 1 , wherein portions of the type program that has been inferred are represented by a set of type tuple constraints (TTCs), wherein each of the TTCs includes:
a tuple of type propositions; an equivalence relation between tuple components; and a set of inhabitation constraints.

6. The computer-implemented method of claim 5 , further comprising:
checking inclusion of a portion of the type program that has been inferred represented by a first set of TTCs into another portion of the type program represented by a second set of TTCs by computing a set of prime implicants of the second set; and checking each TTC in the first set and finding a larger TTC in the set of prime implicants of the second set of TTCs.

7. The computer-implemented method of claim 6 , further comprising:
computing the set of prime implicants of the second set of TTCs by saturating the second set by exhaustively applying consensus operations to ensure all relevant TTCs are included.

8. The computer-implemented method of claim 7 , wherein the consensus operations are performed by
receiving two TTCs as operands; receiving a set of indices and equating all columns whose indices occur in the set, and preserving all other equalities and inhabitation constraints of the operands, and taking disjunctions over columns in the set and conjunctions over all other columns; and taking a union of two or more of the equivalence relations in the operands and a pointwise disjunction of the inhabitation constraints of the operands.

9. The computer-implemented method of claim 8 , further comprising:
reducing a number of consensus operations that need to be performed during saturation by omitting consensus operations where a resulting TTC will be covered by TTCs already present in the set.

10. The computer-implemented method of claim 8 , further comprising:
receiving a logical formula that represents a type hierarchy, and representing a component type proposition of a TTC as a binary decision diagram (BDDs), and choosing a BDD variable order by assigning neighboring indices to type symbols that appear in a same conjunct of the logical formula that represents the type hierarchy.

11. The computer-implemented method of claim 1 , wherein an approximation is used to find erroneous parts of a database query that will return an empty set of results, regardless of contents stored in the database.

12. The computer-implemented method of claim 2 , wherein the providing notification on combining queries by conjunction without creating empty parts in a combined query includes depicting compatible types with similar pictures in a user interface.

13. The computer-implemented method of claim 1 , wherein the one or more queries to the database contain calls to other query procedures, and an approximation is used to optimize these called procedures, by eliminating query parts that will return an empty set of results in a context where they are called, regardless of any contents of the database.

14. The computer-implemented method of claim 13 , wherein the context of a procedure in a database query is computed by
traversing a call graph of that query, and keeping a stack of approximations of all contexts where the procedure is being used, and when entering a procedure in the call graph, pushing a conjunction of an approximation of a body of that procedure and a top of the stack onto the stack as a new context.

15. The computer-implemented method of claim 1 , wherein an approximation is used to optimize queries, by eliminating query parts that test whether a value is included in a portion of the first type program, and the approximation indicates at least one of:
the value will be included in this portion of the first type program regardless of contents stored in the database; and the value will not be included in the portion of the first type program.

16. A system comprising:
a memory; a processor communicatively coupled to the memory; and a type inferencer communicatively coupled to the memory and the processor, wherein the type inferencer is adapted to: accessing a program with one or more query operations to a database that contains relations described by at least one database schema; receiving the database schema and at least one entity type hierarchy for the database; and inferring a first type program from definitions in the program by replacing each use of a database relation in the program by its type in the database schema, and the type is at least portion of a second type program, wherein each of the first type program and the second type program is a derived program using type

Assignees

• Microsoft Technology Licensing Llc

Inventors

• Schaefer Max
• De Moor Oege

Classifications

• G06F8/437 Primary

  Type checking · CPC title

• G06F16/2448 Primary

  for particular applications; for extensibility, e.g. user defined types · CPC title