| Given Input Type | XQuery Expression | Expected Output Type |
<!ELEMENT r (b,c,b*)> <!ELEMENT b EMPTY> <!ELEMENT c EMPTY> |
<r>{for $x in child::* return $x}</r>
|
<!ELEMENT r (b+,c,b*)> <!ELEMENT b EMPTY> <!ELEMENT c EMPTY> |
Explanation
An example discussed in the paper by D. Colazzo and C. Sartiani (PPDP'11). We can observe in this case that backward type inference completely overcomes the precision problems met in approaches based on forward type inference. This is because backward type inference may simply copy portions of the output type into the inferred input type. This is a great advantage in terms of complexity since it avoids an exponential case analysis, and only uses a linear copy instead.
Full Trace
The full trace generated by the implementation for the example above:
Static type-checking 'sample.xq' with input type 'input.dtd' starting at 'r' and output type 'output.dtd' starting at 'r'... Read in sample.xq:{for $x in child::* return $x} Considered Input XQuery expression: element r {for $x in child::* return $x } Parsing tree grammar 'output.dtd'... CFT: 8 type variables, 8 production rules, 3 element names. Resulting CFT is: $Empty -> EMPTYSET $Epsilon -> () $Any -> () $PCData -> () $b -> b(()) $c -> c(()) $1 -> ($b | ($b, $1)) $r -> r((($1, $c), ($1 | ()))) Start symbol is $r 8 type variables, 8 production rules, 3 element names. BTT: 10 type variables, 9 production rules, 4 element names. Resulting BTT is: $Epsilon -> EPSILON $Any -> *($Any, $Any) | EPSILON $Empty -> EMPTYSET $4 -> b($Epsilon, $Epsilon) | b($Epsilon, $4) $3 -> EPSILON | b($Epsilon, $Epsilon) | b($Epsilon, $4) $2 -> c($Epsilon, $3) $5 -> b($Epsilon, $2) | b($Epsilon, $5) $1 -> b($Epsilon, $2) | b($Epsilon, $5) $r -> r($1, $Epsilon) Start Symbol is $r 9 type variables, 9 production rules, 4 element names. Inferring Input Type... elem_elem element r {for $x in child::* return $x } , r($1, $Epsilon) expr_union for $x in child::* return $x , b($Epsilon, $2) | b($Epsilon, $5) for_elem for $x in child::* return $x , b($Epsilon, $2) for_elem returns: (~<-1>T & ~<-2>T & <1>(b & ~<1>T & <2> (let X1=(c & ~<1>T & (~<2>T | <2>X2)), X2=((b & ~<1>T & <2>X2) | (b & ~<1>T & ~<2>T)) in X1))) for_elem for $x in child::* return $x , b($Epsilon, $5) for_elem returns: (~<-1>T & ~<-2>T & <1>(b & ~<1>T & <2> (let X4=((b & ~<1>T & <2>X5) | (b & ~<1>T & <2>X4)), X5=(c & ~<1>T & (<2>X6 | ~<2>T)), X6=((b & ~<1>T & ~<2>T) | (b & ~<1>T & <2>X6)) in X4))) expr_union returns:((~<-1>T & ~<-2>T & <1>(b & ~<1>T & <2> (let X4=((b & ~<1>T & <2>X5) | (b & ~<1>T & <2>X4)), X5=(c & ~<1>T & (<2>X6 | ~<2>T)), X6=((b & ~<1>T & ~<2>T) | (b & ~<1>T & <2>X6)) in X4))) | (~<-1>T & ~<-2>T & <1>(b & ~<1>T & <2> (let X1=(c & ~<1>T & (~<2>T | <2>X2)), X2=((b & ~<1>T & <2>X2) | (b & ~<1>T & ~<2>T)) in X1)))) elem_elem returns: ((~<-1>T & ~<-2>T & <1>(b & ~<1>T & <2> (let X4=((b & ~<1>T & <2>X5) | (b & ~<1>T & <2>X4)), X5=(c & ~<1>T & (<2>X6 | ~<2>T)), X6=((b & ~<1>T & ~<2>T) | (b & ~<1>T & <2>X6)) in X4))) | (~<-1>T & ~<-2>T & <1>(b & ~<1>T & <2> (let X1=(c & ~<1>T & (~<2>T | <2>X2)), X2=((b & ~<1>T & <2>X2) | (b & ~<1>T & ~<2>T)) in X1)))) Inferred input type represented as a formula: ((~<-1>T & ~<-2>T & <1>(b & ~<1>T & <2> (let X4=((b & ~<1>T & <2>X5) | (b & ~<1>T & <2>X4)), X5=(c & ~<1>T & (<2>X6 | ~<2>T)), X6=((b & ~<1>T & ~<2>T) | (b & ~<1>T & <2>X6)) in X4))) | (~<-1>T & ~<-2>T & <1>(b & ~<1>T & <2> (let X1=(c & ~<1>T & (~<2>T | <2>X2)), X2=((b & ~<1>T & <2>X2) | (b & ~<1>T & ~<2>T)) in X1)))) Parsing and compiling input type 'input.dtd' starting at 'r'... Parsing tree grammar 'input.dtd'... CFT: 8 type variables, 8 production rules, 3 element names. Resulting CFT is: $Empty -> EMPTYSET $Epsilon -> () $Any -> () $PCData -> () $b -> b(()) $c -> c(()) $1 -> ($b | ($b, $1)) $r -> r((($b, $c), ($1 | ()))) Start symbol is $r 8 type variables, 8 production rules, 3 element names. BTT: 9 type variables, 8 production rules, 4 element names. Resulting BTT is: $Epsilon -> EPSILON $Any -> *($Any, $Any) | EPSILON $Empty -> EMPTYSET $4 -> b($Epsilon, $Epsilon) | b($Epsilon, $4) $3 -> EPSILON | b($Epsilon, $Epsilon) | b($Epsilon, $4) $2 -> c($Epsilon, $3) $1 -> b($Epsilon, $2) $r -> r($1, $Epsilon) Start Symbol is $r 8 type variables, 8 production rules, 4 element names. Converted tree grammar into BTT [2 ms]. Translated BTT into Tree Logic [2 ms]. input: (let X8=(<1>X9 & r & ~<2>T), X9=(b & ~<1>T & <2>X10), X10=(c & ~<1>T & (<2>X11 | ~<2>T)), X11=((b & ~<1>T & <2>X11) | (b & ~<1>T & ~<2>T)) in X8) neg_inferred: ((mu X14.((~<1>T | <-1>T | <1>(<2> (let X15=((<2>X16 | ~b | <1>T | ~<2>T) & (~b | <2>X15 | <1>T | ~<2>T)), X16=((<2>T & (<2>X17 | ~<2>T)) | ~c | <1>T), X17=((~b | <2>T | <1>T) & (~b | <2>X17 | <1>T | ~<2>T)) in X15) | ~b | <1>T | ~<2>T) | <-2>T) & (~<1>T | <1>(~b | <1>T | ~<2>T | <2> (let X18=(((<2>X19 | ~<2>T) & <2>T) | ~c | <1>T), X19=((~b | <2>T | <1>T) & (~b | <2>X19 | <1>T | ~<2>T)) in X18)) | <-1>T | <-2>T) & (~<1>T | <1>X14) & (<2>X14 | ~<2>T))) | <-1>T | <-2>T) Global formula contains the following total numbers of occurrences (including duplicates): 15 atomic propositions, 58 modalities, 16 variables, 4 fixpoint binder, 32 negations, 12 conjunctions, 19 disjunctions. Satisfiability Tested Formula: (mu X20.((((mu X14.((~<1>T | <-1>T | <1>(<2> (let X15=((<2>X16 | ~b | <1>T | ~<2>T) & (~b | <2>X15 | <1>T | ~<2>T)), X16=((<2>T & (<2>X17 | ~<2>T)) | ~c | <1>T), X17=((~b | <2>T | <1>T) & (~b | <2>X17 | <1>T | ~<2>T)) in X15) | ~b | <1>T | ~<2>T) | <-2>T) & (~<1>T | <1>(~b | <1>T | ~<2>T | <2> (let X18=(((<2>X19 | ~<2>T) & <2>T) | ~c | <1>T), X19=((~b | <2>T | <1>T) & (~b | <2>X19 | <1>T | ~<2>T)) in X18)) | <-1>T | <-2>T) & (~<1>T | <1>X14) & (<2>X14 | ~<2>T))) | <-1>T | <-2>T) & ~<-1>T & (let X8=(<1>X9 & r & ~<2>T), X9=(b & ~<1>T & <2>X10), X10=(c & ~<1>T & (<2>X11 | ~<2>T)), X11=((b & ~<1>T & <2>X11) | (b & ~<1>T & ~<2>T)) in X8) & ~<-2>T & ~<2>T) | <1>X20 | <2>X20)) Warning: no suitable native BDD library found. Falling back to the Java one. Computing Relevant Closure... Computed Relevant Closure [3 ms]. Computed Lean [2 ms]. Lean size is 23. It contains 18 eventualities and 5 symbols. Fixpoint Computation Initialized [15 ms]. Computing Fixpoint.....[28 ms]. Formula is unsatisfiable [53 ms]. Static type checking succeeded! No error detected.