Algebraic Program Analysis Tutorial

2021 CAV Tutorial Introduction to Algebraic Program Analysis Zachary Kincaid Princeton University Thomas Reps University of Wisconsin

Outline Outline Regular algebraic program analysis Semantic foundations of algebraic program analysis Interprocedural analysis ?-regular program analysis 2

How Things Fit Together Program Abstraction engine System of Dataflow Equations Parts 1&2: Intraprocedural analysis Part 3: Interprocedural analysis Part 4: Termination analysis Equation solver Solution (dataflow facts; procedure summaries)

Semantic Equations for Intraprocedural Analysis ? ?,? = ?? ? ?,? = ? ?,?? ?[??,?] ?? ? ? ??,? ????? s x s x m1 ?[s,s] = Id + n mk Susan Graham Mark Wegman 4

Procedure Summaries ? ?,? = a procedure summary An abstraction of the procedure s transition relation s x ?[s,x] + m1 mk 5

start Swap Procedure ?? ( ) void swap(bool p1, bool p2) { if (*) { bool t = p1; p1 = p2; p2 = t; } else { p1 = p1 ^ p2; p2 = p1 ^ p2; p1 = p1 ^ p2; } } ? = ?1 ?1= ?1 ??? ?2 ?1= ?2 ?2= ?1 ??? ?2 ?2= ? ?1= ?1 ??? ?2 ???? 6

Predicate Abstraction (Boolean Programs) post-state assignment (?1 pre-state assignment (?1,?2) ,?2 ) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) ?1 ?1 ??? ?2 ?2 ?1 ??? ?2 ?1 ?1 ??? ?2 1 0 0 0 0 0 0 1 0 0 1 0 0 1 0 0 1 0 0 0 0 1 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 0 0 1 0 0 1 0 0 1 0 0

Three ways to Express Relational Composition Three ways to Express Relational Composition As a logical formula ? ?,? ? ?,? = ? ,?.(? ?,? ?(?,? ) ? = ? ) Two-step reachability in a directed graph = Multiplication of Boolean adjacency matrices 1 0 0 0 0 0 0 1 0 0 1 0 0 1 0 0 1 0 0 0 0 1 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 0 0 1 0 1 0 0 0 0 1 0 = 8

Predicate Abstraction (Boolean Programs) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) ?1 ?1 ??? ?2 ?2 ?1 ??? ?2 ?1 ?1 ??? ?2 1 0 0 0 0 0 0 1 0 0 1 0 0 1 0 0 1 0 0 0 0 1 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 0 0 1 0 0 1 0 0 1 0 0 (00) (01) (10) (11) (00) (01) (10) (11) ?1 ?1 ??? ?2;?2 ?1 ??? ?2 1 0 0 0 0 0 0 1 0 1 0 0 0 0 1 0 9

Predicate Abstraction (Boolean Programs) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) (00) (01) (10) (11) ?1 ?1 ??? ?2 ?2 ?1 ??? ?2 ?1 ?1 ??? ?2 ????(?1,?2) 1 0 0 0 0 0 0 1 0 0 1 0 0 1 0 0 1 0 0 0 0 1 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 0 0 1 0 0 1 0 0 1 0 0 (00) (01) (10) (11) (00) (01) (10) (11) ?1 ?1 ??? ?2;?2 ?1 ??? ?2;?1 ?1 ??? ?2 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 1 10

start Swap Procedure ?? ( ) void swap(bool p1, bool p2) { if (*) { bool t = p1; p1 = p2; p2 = t; } else { p1 = p1 ^ p2; p2 = p1 ^ p2; p1 = p1 ^ p2; } } ? = ?1 ?1= ?1 ??? ?2 ?1= ?2 ?2= ?1 ??? ?2 ?2= ? ?1= ?1 ??? ?2 (00) (00) ? (01) (01) (10) (10) ???? (11) (11) 11

Predicate Abstraction (Boolean Programs) pre-state assignment (?1,?2,?) post-state assignment (?1 ,?2 ,? ) (000) (001) (010) (011) (100) (101) (110) (111) (000) (000) (001) (010) (011) (100) (101) (110) (111) (000) (001) (010) (011) (100) (101) (000) (001) (000) (001) (010) (011) (100) (101) (110) (111) (001) (010) (011) (100) (101) (110) (111) (010) (011) (100) (101) (110) (111) (110) (111) t ?1 ?1 ?2 ?2 ? 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 1 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 1 0 0 0 1 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 12

Predicate Abstraction (Boolean Programs) (000) (001) (010) (011) (100) (101) (110) (111) (000) (000) (001) (010) (011) (100) (101) (110) (111) (000) (001) (010) (011) (100) (101) (000) (001) (000) (001) (010) (011) (100) (101) (110) (111) (001) (010) (011) (100) (101) (110) (111) (010) (011) (100) (101) (110) (111) (110) (111) t ?1 ?1 ?2 ?2 ? 0 1 0 1 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 1 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 1 0 0 0 1 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 (000) (001) (000) (001) (010) (011) (100) (101) (110) (111) (010) (011) (100) (101) (110) (111) 13

Predicate Abstraction (Boolean Programs) (000) (001) (010) (011) (100) (101) (110) (111) (000) (000) (001) (010) (011) (100) (101) (110) (111) (000) (001) (010) (011) (100) (101) (000) (001) (000) (001) (010) (011) (100) (101) (110) (111) (001) (010) (011) (100) (101) (110) (111) (010) (011) (100) (101) (110) (111) (110) (111) t ?1 ?1 ?2 ?2 ? 0 1 0 1 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 1 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 1 0 0 0 1 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 (00) (00) (000) (001) (000) (001) (010) (011) (100) (101) (110) (111) (01) (01) (010) (011) (100) (101) (110) (111) exit scope (10) (10) (11) (11) ????(?1,?2) 1 0 0 0 0 1 0 0 0 1 0 0 0 0 0 1 14

start Swap Procedure ?? ( ) void swap(bool p1, bool p2) { if (*) { bool t = p1; p1 = p2; p2 = t; } else { p1 = p1 ^ p2; p2 = p1 ^ p2; p1 = p1 ^ p2; } } ? = ?1 ?1= ?1 ??? ?2 ?1= ?2 ?2= ?1 ??? ?2 ?2= ? ?1= ?1 ??? ?2 (00) (00) (00) (00) + (01) (01) (01) (01) (10) (10) (10) (10) ???? ?[?????,????] (11) (11) (11) (11) (00) (00) (01) (01) Procedure summary for swap() (10) (10) 15 (11) (11)

Inter Becomes Intra When Procedure Summaries are in Hand x s P ?2 ?1 ?2 ?1 ? ?[? ,? ] ? 16

Inter Becomes Intra When Procedure Summaries are in Hand x s P ?2 ?1 ?2 ?1 Can solve using any intraprocedural method, including the methods from Parts 1 and 2 ??2 ? ? ,? ???2 ? ? ??1 ? ? ,? ???1 17

Inter Becomes Intra When Procedure Summaries are in Hand Works for recursive programs, too! (Use the * operator for both kinds of loops .) x s P ?2 ?1 ?2 ?1 ??2 ? ? ,? ???2 ? ? ??1 ? ? ,? ???1 ?3 ?3 18 ??3 ? ?,? ???3

Two Two- -Phase Phase In Inter terprocedural procedural Analysis Analysis Phase I: Compute procedure summaries Phase II: Create ? = modified interprocedural CFG ? ? For each call-return pair ?,? , insert an edge ? ? labeled with ?? ? ?,? ???, where ? ?,? summarizes the procedure called at ? Remove all ??? edges Solve an intraprocedural -analysis problem on ? What about Phase I? Can use algebraic program analysis for this step! Radhia Cousot 19 Micha Sharir Amir Pnueli Patrick Cousot

Semantic Equations for Interprocedural Analysis, Phase I ? ?,? = ?? ? ?,? = ? ?,?? ?[??,?] ?? ? ? ??,? ????? ? ?,? = ? ?,? ???,? ? ? ,? ???? ,? ? ? s x ?[?,?] m1 s c r x ???,? ???? ,? ? ? + ?[s,s] = Id ?[? ,? ] n mk 20

Phase I: Conventional Approach Set up equation system: ? ?,? = ?? ??? ??? ? ?????????? ? ?,? = ? ?,?? ?[??,?] ??? ??? ? ?????????? ? ?????????? ??,? ????? Summary for called procedure ? ?,? = ? ?,? ???,? ? ? ,? ???? ,? ??? ??? ?,? ????????? ?,? ????? Summary for call site Solve using successive approximation (Kleene evaluation or chaotic iteration) 21

Remainder of Part 3: Remainder of Part 3: Algebraic Program Analysis for Phase I Algebraic Program Analysis for Phase I Phase Non-Recursive Programs Recursive Programs Phase I Partial story Phase II Where we are headed: Describe a method for Phase I for recursive programs It is an iterative analysis that makes repeated calls on an algebraic program analysis 22

Four Simple Facts about Formal Languages Four Simple Facts about Formal Languages (Intro Theory Class, week ~4) (Intro Theory Class, week ~4) Regular languages (???) versus linear context-free languages (LCFL) 1. ? ??? = ? ?????? = ??? 2. For a left-linear context-free grammar ?, ? ??? E.g., for ? = ? ? ? ? ?, ? = ? + ? ??? 3. For the linear context-free grammar ? = ? ? ? | ?, ? = ???? ??? 4. For the linear context-free grammar ? = ?1 ? ?1 | ?2 ? ?2 | ?, ? = ,?1?2?2?1,?2?1?1?2,?2?1?2?2?1?2, ??? 23

Ingredients of the Story Regular languages LCFLs, such as ???? Gottfried Wilhelm Leibniz Isaac Newton 24

Story in a Nutshell Story in a Nutshell In 1981, Tarjan found a fast way to solve intraprocedural dataflow equations ( algebraic program analysis ) Solves a linear system of equations In 2008, Esparza et al. used inspiration from Newton s Method to solve interprocedural dataflow equations Repeatedly: create and solve a linear system of equations Esparza et al. and Tarjan do not create the same type of linear system Cannot apply Tarjan smethods to Esparza et al. s linear systems In 2016, Reps et al. found a way to transform Esparza et al. s linear systems so that Tarjan s approach can be applied Surprising because a reasonable-sounding sanity check suggests that such a transformation is not possible! 25

Outline Outline Newtonian program analysis Iterative analysis that makes repeated calls on an iterative program analysis Newtonian program analysis via tensor product Iterative analysis that makes repeated calls on an algebraic program analysis 27

Newtons Method Newton s Method for Finding Roots for Finding Roots y A way to find successively better approximations of a root of a function f(xi) f(xi+1) Given a function f, its derivative f and an initial x0, repeatedly perform x xi+1 xi xi+2 Newtonian Program Analysis: The same general idea repeatedly create and solve a linear model can be applied to programs, too Create a linear model of the function and use it to find a better approximation of the solution ? ?? ? ?? ??+1= ?? Isaac Newton 28

Newtonian Program Analysis Kleene iteration ?(0)= ?(0) ?(?+1)= ?( ?(?)) NPA iteration ?(0) = ?(0) ?(?+1)= ? ?? + ???????????????????? ?, ?(?)

Newtonian Program Analysis Kleene iteration ?(0)= ?(0) ?(?+1)= ?( ?(?)) NPA iteration ?(0) = ?(0) ?(?+1)= ? ?? + ???????????????????? ?, ?(?) Non-numeric equations with a commutative multiplication Numeric equations from probabilistic programs Dexter Kozen Mark Hopkins Mihalis Yannakakis Kousha Etessami 30 30

Newtonian Program Analysis Kleene iteration ?(0)= ?(0) ?(?+1)= ?( ?(?)) NPA iteration ?(0) = ?(0) ?(?+1)= ? ?? + ???????????????????? ?, ?(?) Non-numeric equations from interprocedural dataflow analysis: non-commutative multiplication 31 Javier Esparza Michael Luttenberger Stefan Kiefer 31

Newtonian Program Analysis Newtonian Program Analysis Esparza et al. had to finesse certain differences Real-valued equations Algebraic semiring Mathematics Multiplication: x Program Analysis Abstract Compose: Abstract Union: + Addition: + 32

Polynomial Equations Polynomial Equations for Summary Functions for Summary Functions proc X1 proc X2 x1() { a; x2(); } x2() { if (*) d; else{ b; x2(); x2(); c; } } b a X2 X2 d X2 X2 c Equation System ?1= ? ?2 ?2= ? +? ?2 ?2 ? 33

Polynomial Equations Polynomial Equations for Summary Functions for Summary Functions proc X1 proc X2 x1() { a; x2(); } x2() { if (*) d; else{ b; x2(); x2(); c; } } b a X2 X2 d X2 c Equation System This term is quadratic ?1= ? ?2 ?2= ? +? ?2 ?2 ? 34

Problematic Issues . . . Problematic Issues . . . We have no minus operation in dataflow analysis ? ? ? = 0 ?(?) = ? What the heck do we do about ? ? ? ?? ? ?? ??+1= ?? 35

Newtonian Program Analysis Newtonian Program Analysis Leibniz product rule Gottfried Wilhelm Leibniz Finesse the derivative question by fiat: ? ? + = ?? + ? ? ? = ?? + ? ? Outer fixpoint computation Really a differential: ? ? NPA iteration ?(0) = ?(0) ?(?+1)= ?(?) where ?(?) is the least solution of ? = ? ?? + ? ?|?? (?) ? ?? |?? ? + ? ? ??|???.? ? ?, modulo non-commutativity of if ?(?) is a constant if ?(?) = ? if ? ? = ? ? + (?) if ? ? = ? ? (?) 0 ? ?? ? |?? + ? (?)|?? ?? ? |?? ? ??(?)|?? = Inner fixpoint computation Example 1: ? ? + ? ? ? ? |?? Linear correction term ? ???? |?? ? ? ? + ? ? ? ? Example 2: ? ? ? ? 36

Polynomial Equations Polynomial Equations for Summary Functions for Summary Functions Differentiated equations Original equations ?1= ? ?2 +? ?2 ?2= ? + ? ?2 ?2 ? + ? ?2 ?2 ? + ? ?2 ?2 ? Apply the linearization operator ?1= ? ?2 ?2= ? +? ?2 ?2 ? y Each summand now only has one variable; this system of equations is linear! proc X1 proc X2 f(xi) b a ?2 is the value of ?2 from the previous Newton round i.e., some constant for the current round X2 X2 xi x d xi+1 xi+2 X2 c 37

Polynomial Equations Polynomial Equations for Summary Functions for Summary Functions Differentiated equations Original equations ?1= ? ?2 +? ?2 ?2= ? + ? ?2 ?2 ? + ? ?2 ?2 ? + ? ?2 ?2 ? procY1 Apply the linearization operator ?1= ? ?2 ?2= ? + ? ?2 ?2 ? proc X1 Operational interpretation: ?2 is the current approximation At first call, use ?2; at second call, perform exploration (of the transformed procedure) At first call, perform exploration (of the transformed procedure); at second call, use ?2 Combine results (+) proc Y2 proc X2 a a b b b b a y2 y2 Y2 y2 X2 X2 Y2 d d X2 y2 Y2 y2 c c c c 38

Goal: Solve Linear Equations Precisely Goal: Solve Linear Equations Precisely Given ??= ??+ ?,???,?,? ?? ??,?,? Find ? Pre-call action Post-call action Can we find ? using algebraic program analysis? 39

Goal: Analyze Linearly Recursive Programs Precisely Goal: Analyze Linearly Recursive Programs Precisely int a, b; int foo() { if (*) { a = a+1; foo(); b = b+1; } return; } Pre-call action Post-call action 40

Outline Outline Newtonian program analysis Iterative analysis that makes repeated calls on an iterative program analysis Newtonian program analysis via tensor product Iterative analysis that makes repeated calls on an algebraic program analysis 41

A Misconception on My Part Polynomial Linear Interprocedural analysis Intraprocedural analysis On each Newton round, use a fast intraprocedural solver, such as Tarjan s path-expression method! 43

A Misconception on My Part A Misconception on My Part Issue: Extend ( ) typically models the reversal of function composition: ? ? ? ? In general, is not commutative In a semiring ? ?2|?(?) = ? ? ? |?(?) = ? ? |?? ? + ? ? ? |?? =? ? + ? ? ? ? + ? ? In calculus ? ?2|?(?) = ? ? ? |?(?) = =? ? +? ? = ? ? + ? ? = 2?? ? ? |?? ? +? ? ? |?? ? ?2 ?2 ? ?2 ? ?2 ? b ?2 ? ?2 = 2??? Esparza s linear equations are not left-linear or right- linear, which Tarjan requires 45

Doesnt the Pumping Lemma Doesn t the Pumping Lemma Imply . . . Imply . . . Fuggedaboutit Fuggedaboutit? ? If we represent the Esparza linearized system as a grammar, we obtain a linear context-free grammar ?1 = ??2 | ??2 ?2 = ? | ??2?2? ??2?2? ??2?2? One learns early on in a formal-language course that not all languages defined by a linear context-free grammar are regular In particular, { ???? | ? ? } is the canonical example of an LCFL language that is not regular: X ::= a X b | Suggests that we are barking up the wrong tree . . . Michael Rabin Dana Scott

Sanity Check? Tarjan s path-expression method (a technique based on Regular languages) LCFLs from NPA Regular languages 47

Doesnt the Pumping Lemma Doesn t the Pumping Lemma Imply . . . Imply . . . Fuggedaboutit Fuggedaboutit? ? If we represent the Esparza linearized system as a grammar, we obtain a linear context-free grammar ?1 = ??2 | ??2 ?2 = ? | ??2?2? ??2?2? ??2?2? One learns early on in a formal-language course that not all languages defined by a linear context-free grammar are regular In particular, { ???? | ? ? } is the canonical example of an LCFL language that is not regular: X ::= a X b | Suggests that we are barking up the wrong tree . . . But we aren t! We can sidestep the issue with some magic from algebra Michael Rabin Dana Scott 48

Converting to Converting to Tarjan Tarjan The challenge: Devise a way to accumulate matching quantities on both the left and right sides However, in a regular language, we can only accumulate values on one side Suggests using pairs of values (lhs, rhs): ?1= ? ?2 +? ?2 ?2= ? + ? ?2 ?2 ? + ? ?2 ?2 ? + ? ?2 ?2 ? becomes ?1= (1,? ?2) ?1= (?1) ??2 ?(?,1) ?2= (?2) ?2= (1,?) ?(1,? ?2 ?2 ?) ??2 ?(? ?2,?) ??2 ?(?,?2 ?) LCFL Each variable occurrence is now leftmost in its summand; this system of equations is left-linear! Left-recursive = Regular 49

Converting to Converting to Tarjan Tarjan The challenge: Devise a way to accumulate matching quantities on both the left and right sides However, in a regular language, we can only accumulate values on one side Suggests using pairs of values (lhs, rhs): ?1,?1 ??2,?2 =?? ?1+ ?2,?1+ ?2 ?1,?1 ??2,?2 =?? ?2 ?1,?1 ?2 Given a pair ?,? , define the readout operation ( ?,? ) ? ? Thus, ( ?1,?1 ??2,?2) = ( ?1,?1 ??2,?2) = ( ?2 ?1,?1 ?2) =?2 ?1 ?1 ?2 50

Converting to Converting to Tarjan Tarjan The challenge: Devise a way to accumulate matching quantities on both the left and right sides However, in a regular language, we can only accumulate values on one side (1,? ?2)?1= (?1) ?1= ? ?2 ?1= +? ?2 ?2= ? + ? ?2 ?2 ? + ? ?2 ?2 ? ? ?2 ??,1 ?2= (2) ?2 = (?2) (3) (3) (1,?) ? (1,? ?2 ?2 ?) ??2 ?(? ?2,?) ??2 ?(?,?2 ?) (1) (1) (2) + ? ?2 ?2 ? (1,d) b d b (b, y2 c) (b y2, c) y2 y2 ((1,d) ?(b,y2 c) ?(b y2,c)) = (b y2 b 1, d y2 c c) = b y2 b 1 d y2 c c (1,d) ?(b,y2 c) ?(b y2,c) c c 51

Pairing Fails to Deliver . . . a1 Y1 b1 a2 Y1 b2 Z1 p (a1, b1) Y1= 1 Y2= Z1= (1, 1) pZ1 p (a2, b2) Z2= proc Y1 proc Y2 proc Z1 proc Z2 Z1 Z1 a1 a2 1 (1,1) Y1 Y1 (a1, b1) (a2,b2) Least solution ( pof the two paths): Z2= (1,1) ? (a1, b1) p(1,1) ? (a2, b2) = (a1, b1) p(a2, b2) = a1+ a2,b1+ b2 b1 b2 Least solution (+ of the two paths): Y2= a1 1 b1+ a2 1 b2 = a1b1+ a2b2 ((a1+a2, b1+b2)) = (a1+a2) (b1+b2) = a1b1 +a2b1 +a1b2 +a2b2 Conservative, but loses precision . . . 52

Doesnt the Pumping Lemma Doesn t the Pumping Lemma Imply . . . Imply . . . Fuggedaboutit Fuggedaboutit? ? If we represent the Esparza linearized system as a grammar, we obtain a linear context-free grammar ?1 = ??2 | ??2 ?2 = ? | ??2?2? ??2?2? ??2?2? One learns early on in a formal-language course that not all languages defined by a linear context-free grammar are regular In particular, { aibi | i N } is the canonical example of an LCFL language that is not regular: X ::= a X b | Suggests that we are barking up the wrong tree . . . Michael Rabin Dana Scott 53