LP (the Larch Prover), Release 3.1a (95/04/27) logging to `/pro/oodb/specs/KOLA98/snf-scripts.lplog' on 21 June 1998 18:56:45. LP0.1.2: LP0.1.3: % ****************************************************************************** LP0.1.4: % * * LP0.1.5: % * Script File: SIGMOD98_Scripts * LP0.1.6: % * -------------------------------------------------------------------------- * LP0.1.7: % * Scripts Author: Mitch Cherniack (mfc@cs.brandeis.edu) * LP0.1.8: % * Date: June, 1998 * LP0.1.9: % * * LP0.1.10: % * Present Address: Computer Science Department * LP0.1.11: % * Brandeis University * LP0.1.12: % * Waltham, MA 02254 * LP0.1.13: % * -------------------------------------------------------------------------- * LP0.1.14: % * * LP0.1.15: % * Proof Scripts Establishing Correctness of Rewrite Rules used in the paper, * LP0.1.16: % * [CZ98a]: * LP0.1.17: % * * LP0.1.18: % * [CZ98a] Changing the Rules: Transformations for Rule-Based Optimizers * LP0.1.19: % * Mitch Cherniack and Stan Zdonik, In Proceedings of the 1998 ACM * LP0.1.20: % * SIGMOD International Conference on Management of Data, Seattle, * LP0.1.21: % * WA, June, 1998. * LP0.1.22: % * * LP0.1.23: % * For an up-to-date version of [CZ98a], see: * LP0.1.24: % * ftp://wilma.cs.brown.edu/u/mfc/sigmod98.ps.Z * LP0.1.25: % * * LP0.1.26: % * * LP0.1.27: % * Instructions: * LP0.1.28: % * * LP0.1.29: % * Requires Version 3.1a of the LP Theorem Prover, available from * LP0.1.30: % * MIT, Laboratory of Computer Science. For software and documentation on * LP0.1.31: % * LP see: * LP0.1.32: % * * LP0.1.33: % * http://www.sds.lcs.mit.edu/spd/larch/LP/overview.html * LP0.1.34: % * * LP0.1.35: % * With LP installed in $path, run this theorem prover script by typing * LP0.1.36: % * * LP0.1.37: % * $path/lp -c SIGMOD98_Scripts * LP0.1.38: % * * LP0.1.39: % ****************************************************************************** LP0.1.40: LP0.1.41: % Section 2: SNF LP0.1.42: % LP0.1.43: % Proof Scripts for COKO Transformations, LP0.1.44: % LP0.1.45: % TRANSFORMATION SNF LP0.1.46: % USES LP0.1.47: % SimpLits, LP0.1.48: % CNF, LP0.1.49: % OrderConjs, LP0.1.50: % pushneg: ~ (p OPLUS f) --> (~ (p)) OPLUS f, LP0.1.51: % init: p --> (K (true) OPLUS #1) & (K (true) OPLUS #2) & K (true) & p, LP0.1.52: % pull: (p OPLUS f) | (q OPLUS f) --> (p | q) OPLUS f, LP0.1.53: % shift: p & (q & r) --> (p & r) & q, LP0.1.54: % simplify: K (true) & p --> p LP0.1.55: % BEGIN LP0.1.56: % SimpLits; LP0.1.57: % CNF; LP0.1.58: % TD {pushneg}; LP0.1.59: % init; LP0.1.60: % BU {pull || {REPEAT shift}}; LP0.1.61: % OrderConjs; LP0.1.62: % BU {simplify} LP0.1.63: % END LP0.1.64: % LP0.1.65: % TRANSFORMATION SimpLits LP0.1.66: % USES LP0.1.67: % SL1: --> o h, LP0.1.68: % SL2: --> K ([x, y]), LP0.1.69: % SL3: --> o f, LP0.1.70: % SL4: --> o f, LP0.1.71: % SL5: f o (g o h) --> (f o g) o h, LP0.1.72: % SL6: f o K (x) --> K (f ! x), LP0.1.73: % SL7: p OPLUS (f o g) --> p OPLUS f OPLUS g, LP0.1.74: % SL8: p OPLUS K (x) --> K (p ? x) LP0.1.75: % BEGIN LP0.1.76: % BU {{{SL1 || SL2 || SL3 || SL4} -> LP0.1.77: % {REPEAT {SL5 -> {print "SL5 fired on"; LP0.1.78: % GIVEN f DO print f; print "\n"}}}} || LP0.1.79: % SL6 || SL7 || SL8} LP0.1.80: % END LP0.1.81: % LP0.1.82: % TRANSFORMATION OrderConjs LP0.1.83: % USES LP0.1.84: % OC1: (p OPLUS #1) & q & r & (r' OPLUS #1) --> ((p & r') OPLUS #1) & q & r, LP0.1.85: % OC2: p & (q OPLUS #2) & r & (r' OPLUS #2) --> p & ((q & r') OPLUS #2) & r, LP0.1.86: % OC3: p & q & r & r' --> p & q & (r & r') LP0.1.87: % BEGIN LP0.1.88: % BU {OC1 || OC2 || OC3} LP0.1.89: % END LP0.1.90: % LP0.1.91: % In [CZ98a], transformation SNF does not contain the rewrite rule, LP0.1.92: % pushneg, nor the firing algorithm statement, LP0.1.93: % LP0.1.94: % TD {pushneg} LP0.1.95: % LP0.1.96: LP0.1.97: LP0.1.98: clear LP0.1.99: set order manual The ordering-method is now `manual'. LP0.1.100: exec-silently SNF_Aux_Axioms End of input from file `/pro/oodb/specs/KOLA98/SNF_Aux_Axioms.lp'. LP0.1.101: set order noeq-dsmpos The ordering-method is now `noeq-dsmpos'. LP0.1.102: order formulas The system now contains 66 rewrite rules. The rewriting system is guaranteed to terminate. All equations have been oriented into rewrite rules. The rewriting system is guaranteed to terminate. LP0.1.103: make immune formulas LP0.1.104: LP0.1.105: % L1: Rules Used in Transformation, SNF LP0.1.106: % ------------------------------------- LP0.1.107: LP0.1.108: set name pushneg The name-prefix is now `pushneg'. LP0.1.109: declare variables p: pred [S], f: fun [R, S] LP0.1.110: prove ~ (p \oplus f) = (~ (p) \oplus f) Attempting to prove conjecture pushneg.1: ~(p \oplus f) = (~p) \oplus f Conjecture pushneg.1 [] Proved by normalization. Deleted formula pushneg.1, which reduced to `true'. LP0.1.111: qed All conjectures have been proved. LP0.1.112: LP0.1.113: set name init The name-prefix is now `init'. LP0.1.114: declare variables p: pred [pair [T, U]] LP0.1.115: prove p = (K (true) \oplus fst) & (K (true) \oplus snd) & K (true) & p Attempting to prove conjecture init.1: p = (K(true) \oplus fst) & (K(true) \oplus snd) & K(true) & p Conjecture init.1 [] Proved by normalization. Deleted formula init.1, which reduced to `true'. LP0.1.116: qed All conjectures have been proved. LP0.1.117: LP0.1.118: set name pull The name-prefix is now `pull'. LP0.1.119: declare variables p: pred [S], f: fun [R, S] LP0.1.120: prove (p \oplus f) | (q \oplus f) = (p | q) \oplus f Attempting to prove conjecture pull.1: (p \oplus f) | (q \oplus f) = (p | q) \oplus f Conjecture pull.1 [] Proved by normalization. Deleted formula pull.1, which reduced to `true'. LP0.1.121: qed All conjectures have been proved. LP0.1.122: LP0.1.123: set name shift The name-prefix is now `shift'. LP0.1.124: declare variables p, q, r: pred [S] LP0.1.125: prove p & (q & r) = (p & r) & q Attempting to prove conjecture shift.1: p & (q & r) = p & r & q Conjecture shift.1 [] Proved by normalization. Deleted formula shift.1, which reduced to `true'. LP0.1.126: qed All conjectures have been proved. LP0.1.127: LP0.1.128: set name simplify The name-prefix is now `simplify'. LP0.1.129: declare variables p: pred [S] LP0.1.130: prove K (true) & p: pred [S] = p Attempting to prove conjecture simplify.1: (K(true) & p):pred[S] = p Conjecture simplify.1 [] Proved by normalization. Deleted formula simplify.1, which reduced to `true'. LP0.1.131: qed All conjectures have been proved. LP0.1.132: LP0.1.133: % L1: Rules Used in Transformation, SimpLits LP0.1.134: % ------------------------------------------ LP0.1.135: LP0.1.136: set name SL1 The name-prefix is now `SL1'. LP0.1.137: declare variables h: fun [T, U], f: fun [U, V], g: fun [U, W] LP0.1.138: prove \< f \circ h, g \circ h \> = \< f, g \> \circ h Attempting to prove conjecture SL1.1: \ = \ \circ h Conjecture SL1.1 [] Proved by normalization. Deleted formula SL1.1, which reduced to `true'. LP0.1.139: qed All conjectures have been proved. LP0.1.140: LP0.1.141: set name SL2 The name-prefix is now `SL2'. LP0.1.142: declare variables x: U, y: V LP0.1.143: prove \< K (x), K (y) \> = K ([x, y]) Attempting to prove conjecture SL2.1: \ = K([x, y]) Conjecture SL2.1 [] Proved by normalization. Deleted formula SL2.1, which reduced to `true'. LP0.1.144: qed All conjectures have been proved. LP0.1.145: LP0.1.146: set name SL3 The name-prefix is now `SL3'. LP0.1.147: declare variables x: V, f: fun [T, U] LP0.1.148: prove \< f, K (x) \> = \< id, K (x) \> \circ f Attempting to prove conjecture SL3.1: \ = \ \circ f Conjecture SL3.1 [] Proved by normalization. Deleted formula SL3.1, which reduced to `true'. LP0.1.149: qed All conjectures have been proved. LP0.1.150: LP0.1.151: set name SL4 The name-prefix is now `SL4'. LP0.1.152: declare variables x: V, f: fun [T, U] LP0.1.153: prove \< K (x), f \> = \< K (x), id \> \circ f Attempting to prove conjecture SL4.1: \ = \ \circ f Conjecture SL4.1 [] Proved by normalization. Deleted formula SL4.1, which reduced to `true'. LP0.1.154: qed All conjectures have been proved. LP0.1.155: LP0.1.156: set name SL5 The name-prefix is now `SL5'. LP0.1.157: declare variables h: fun [T, U], g: fun [U, V], f: fun [V, W] LP0.1.158: prove f \circ (g \circ h) = (f \circ g) \circ h Attempting to prove conjecture SL5.1: f \circ (g \circ h) = f \circ g \circ h Conjecture SL5.1 [] Proved by normalization. Deleted formula SL5.1, which reduced to `true'. LP0.1.159: qed All conjectures have been proved. LP0.1.160: LP0.1.161: set name SL6 The name-prefix is now `SL6'. LP0.1.162: declare variables x: U, f: fun [U, V] LP0.1.163: prove f:fun [U, V] \circ K (x) = K (f:fun [U, V] ! x) Attempting to prove conjecture SL6.1: (f \circ K(x)):fun[T, V] = K(f:fun[U, V] ! x) Conjecture SL6.1 [] Proved by normalization. Deleted formula SL6.1, which reduced to `true'. LP0.1.164: qed All conjectures have been proved. LP0.1.165: LP0.1.166: set name SL7 The name-prefix is now `SL7'. LP0.1.167: declare variables g: fun [T, U], f: fun [U, V], p: pred [V] LP0.1.168: prove p \oplus (f \circ g) = (p \oplus f) \oplus g Attempting to prove conjecture SL7.1: p \oplus (f \circ g) = p \oplus f \oplus g Conjecture SL7.1 [] Proved by normalization. Deleted formula SL7.1, which reduced to `true'. LP0.1.169: qed All conjectures have been proved. LP0.1.170: LP0.1.171: set name SL8 The name-prefix is now `SL8'. LP0.1.172: declare variables x: U, p: pred [U] LP0.1.173: prove p: pred [U] \oplus K (x) = K (p: pred [U] ? x) Attempting to prove conjecture SL8.1: (p:pred[U] \oplus K(x)):pred[T] = K(p:pred[U] ? x) Conjecture SL8.1 [] Proved by normalization. Deleted formula SL8.1, which reduced to `true'. LP0.1.174: qed All conjectures have been proved. LP0.1.175: LP0.1.176: % L1: Rules Used in Transformation, OrderConjs LP0.1.177: % -------------------------------------------- LP0.1.178: LP0.1.179: set name OC1 The name-prefix is now `OC1'. LP0.1.180: declare variables p: pred [T], q: pred [U], r: pred [pair [T, U]], s: pred [T] .. LP0.1.181: prove (p \oplus fst) & (q \oplus snd) & r & (s \oplus fst) = ((p & s) \oplus fst) & (q \oplus snd) & r .. Attempting to prove conjecture OC1.1: (p \oplus fst) & (q \oplus snd) & r & (s \oplus fst) = ((p & s) \oplus fst) & (q \oplus snd) & r Conjecture OC1.1 [] Proved by normalization. Deleted formula OC1.1, which reduced to `true'. LP0.1.182: qed All conjectures have been proved. LP0.1.183: LP0.1.184: set name OC2 The name-prefix is now `OC2'. LP0.1.185: declare variables p: pred [T], q: pred [U], r: pred [pair [T, U]], s: pred [U] LP0.1.186: prove (p \oplus fst) & (q \oplus snd) & r & (s \oplus snd) = (p \oplus fst) & ((q & s) \oplus snd) & r .. Attempting to prove conjecture OC2.1: (p \oplus fst) & (q \oplus snd) & r & (s \oplus snd) = (p \oplus fst) & ((q & s) \oplus snd) & r Conjecture OC2.1 [] Proved by normalization. Deleted formula OC2.1, which reduced to `true'. LP0.1.187: qed All conjectures have been proved. LP0.1.188: LP0.1.189: set name OC3 The name-prefix is now `OC3'. LP0.1.190: declare variables p: pred [T], q: pred [U], r, s: pred [pair [T, U]] LP0.1.191: prove (p \oplus fst) & (q \oplus snd) & r & s = (p \oplus fst) & (q \oplus snd) & (r & s) .. Attempting to prove conjecture OC3.1: (p \oplus fst) & (q \oplus snd) & r & s = (p \oplus fst) & (q \oplus snd) & (r & s) Conjecture OC3.1 [] Proved by normalization. Deleted formula OC3.1, which reduced to `true'. LP0.1.192: qed All conjectures have been proved. LP0.1.193: LP0.1.194: quit End of input from file `/pro/oodb/specs/KOLA98/snf-scripts.lp'. End of input from file `command line arguments'.