IP Library Granted Patent US 9,996,583
Granted Patent B1
US 9,996,583 · App. 15/605,134 · Granted Jun 12, 2018

Differential recursive evaluation of recursive aggregates

Inventor: Michael Peyton Jones (Oxford, GB)
Assignee: Semmle Limited
G06F17/30513G06F17/30327G06F17/30554
View Patent ↗
Loading inventors, assignments & file history…
Monitor This Case
Get email alerts when status or documents change.
Order Certified Copies
Most orders are placed with the USPTO same day — all within 24 business hours.
Order via The Patent Place →
Pre-filled with this patent's details
Quick Facts
Patent No.
US 9,996,583
App. No.
15/605,134
Granted
Jun 12, 2018
Kind
B1
Abstract

Methods, systems, and apparatus, including computer programs encoded on computer storage media, for performing differential recursive evaluation of recursive aggregates. One of the methods includes receiving an original recursive expression that defines tuples belonging to an output relation, wherein the original recursive expression has a recursive aggregation construct, the recursive aggregation construct having a range and a recursive term. An aggregates delta rule is applied to the initial delta expression to generate a final delta expression having an existential term and a gamma term. The existential term is evaluated to generate tuples related by the range and tuples in the delta relation, and the aggregation construct is evaluated using tuples generated by the existential term as the range of the aggregation construct. The output relation is updated including adding to the output relation any tuples newly generated by evaluating the final delta expression.

Claims (62)

1. A system comprising:

one or more computers and one or more storage devices storing instructions that are operable, when executed by the one or more computers, to cause the one or more computers to perform operations comprising:

receiving an original recursive expression that defines tuples belonging to an output relation, wherein the original recursive expression has a recursive aggregation construct, the recursive aggregation construct having a range and a recursive term;

generating an initial delta expression from the original recursive expression;

generating a final delta expression including repeatedly applying one or more differential rules to the initial delta expression, including applying an aggregates delta rule to generate a conjunction of:

(i) an existential term having a subterm that is a conjunction of the range and a delta term that is the recursive term of the aggregation construct, and

(ii) a gamma term having a subterm that is the aggregation construct;

evaluating the original recursive expression on an initial condition to generate one or more tuples;

computing an initial delta relation as a difference between the one or more tuples and the initial condition; and

until the final delta expression generates no new tuples, performing operations comprising:

evaluating the existential term to generate tuples related by the range and tuples in the delta relation,

evaluating the aggregation construct using tuples generated by the existential term as the range of the aggregation construct, and

updating the output relation including adding to the output relation any tuples newly generated by evaluating the final delta expression.

2. The system of claim 1 , wherein evaluating the aggregation construct comprises evaluating the aggregation construct if and only if the existential term generates one or more tuples.

3. The system of claim 2 , wherein the operations further comprise evaluating the existential term before the aggregation construct.

4. The system of claim 1 , wherein the operations further comprise:

applying an aggregates epsilon rule to the initial delta expression to generate an epsilon expression having a conjunction of:

(i) an existential term having a subterm that is a conjunction of the range and an epsilon term having a subterm that is the recursive term of the aggregation construct, and

(ii) a gamma term having a subterm that is the aggregation construct.

5. The system of claim 4 , wherein updating the output relation comprises evaluating the epsilon expression and removing from the output relation any tuples generated by the final epsilon expression.

6. The system of claim 1 , wherein the original recursive expression defines a height, a depth, or a number of nodes in a tree-structured graph.

7. A computer-implemented method comprising:

receiving an original recursive expression that defines tuples belonging to an output relation, wherein the original recursive expression has a recursive aggregation construct, the recursive aggregation construct having a range and a recursive term;

receiving an original recursive expression that defines tuples belonging to an output relation, wherein the original recursive expression has a recursive aggregation construct, the recursive aggregation construct having a range and a recursive term;

generating an initial delta expression from the original recursive expression;

generating a final delta expression including repeatedly applying one or more differential rules to the initial delta expression, including applying an aggregates delta rule to generate a conjunction of:

(i) an existential term having a subterm that is a conjunction of the range and a delta term that is the recursive term of the aggregation construct, and

(ii) a gamma term having a subterm that is the aggregation construct;

evaluating the original recursive expression on an initial condition to generate one or more tuples;

computing an initial delta relation as a difference between the one or more tuples and the initial condition; and

until the final delta expression generates no new tuples, performing operations comprising:

evaluating the existential term to generate tuples related by the range and tuples in the delta relation,

evaluating the aggregation construct using tuples generated by the existential term as the range of the aggregation construct, and

updating the output relation including adding to the output relation any tuples newly generated by evaluating the final delta expression.

8. The method of claim 7 , wherein evaluating the aggregation construct comprises evaluating the aggregation construct if and only if the existential term generates one or more tuples.

9. The method of claim 8 , further comprising evaluating the existential term before the aggregation construct.

10. The method of claim 7 , further comprising:

applying an aggregates epsilon rule to the initial delta expression to generate an epsilon expression having a conjunction of:

(i) an existential term having a subterm that is a conjunction of the range and an epsilon term having a subterm that is the recursive term of the aggregation construct, and

(ii) a gamma term having a subterm that is the aggregation construct.

11. The method of claim 10 , wherein updating the output relation comprises evaluating the epsilon expression and removing from the output relation any tuples generated by the final epsilon expression.

12. The method of claim 7 , wherein the original recursive expression defines a height, a depth, or a number of nodes in a tree-structured graph.

13. A computer program product, encoded on one or more non-transitory computer storage media, comprising instructions that when executed by one or more computers cause the one or more computers to perform operations comprising:

receiving an original recursive expression that defines tuples belonging to an output relation, wherein the original recursive expression has a recursive aggregation construct, the recursive aggregation construct having a range and a recursive term;

generating an initial delta expression from the original recursive expression;

generating a final delta expression including repeatedly applying one or more differential rules to the initial delta expression, including applying an aggregates delta rule to generate a conjunction of:

(i) an existential term having a subterm that is a conjunction of the range and a delta term that is the recursive term of the aggregation construct, and

(ii) a gamma term having a subterm that is the aggregation construct;

evaluating the original recursive expression on an initial condition to generate one or more tuples;

computing an initial delta relation as a difference between the one or more tuples and the initial condition; and

until the final delta expression generates no new tuples, performing operations comprising:

evaluating the existential term to generate tuples related by the range and tuples in the delta relation,

evaluating the aggregation construct using tuples generated by the existential term as the range of the aggregation construct, and

updating the output relation including adding to the output relation any tuples newly generated by evaluating the final delta expression.

14. The computer program product of claim 13 , wherein evaluating the aggregation construct comprises evaluating the aggregation construct if and only if the existential term generates one or more tuples.

15. The computer program product of claim 14 , wherein the operations further comprise evaluating the existential term before the aggregation construct.

16. The computer program product of claim 13 , wherein the operations further comprise:

applying an aggregates epsilon rule to the initial delta expression to generate an epsilon expression having a conjunction of:

(i) an existential term having a subterm that is a conjunction of the range and an epsilon term having a subterm that is the recursive term of the aggregation construct, and

(ii) a gamma term having a subterm that is the aggregation construct.

17. The computer program product of claim 16 , wherein updating the output relation comprises evaluating the epsilon expression and removing from the output relation any tuples generated by the final epsilon expression.

18. The computer program product of claim 13 , wherein the original recursive expression defines a height, a depth, or a number of nodes in a tree-structured graph.

Assignments (3)
ASSIGNMENT OF ASSIGNOR'S INTEREST Recorded Jan 27, 2020
From: GITHUB SOFTWARE UK LTD.
To: MICROSOFT TECHNOLOGY LICENSING, LLC
Reel/Frame 051710/0252 →
CHANGE OF NAME Recorded Dec 11, 2019
From: SEMMLE LTD.
To: GITHUB SOFTWARE UK LTD.
Reel/Frame 052027/0912 →
ASSIGNMENT OF ASSIGNOR'S INTEREST Recorded Jul 7, 2017
From: JONES, MICHAEL PEYTON
To: SEMMLE LIMITED
Reel/Frame 043116/0896 →