haskell-te: 7b950a6731effcd3b2bfeb5a8c8bfc0f791330cb
1: From: Chris Warburton
2: Date: Wed, 15 Nov 2017 17:21:27 +0000
3: State: resolved
4: Subject: Handle 'lambda' and '@' in TIP theorems
5: Message-Id: <f5669cd4db415d36-0-artemis@nixos>
6: resolution: fixed
7:
8: Consider the following puported TIP theorem:
9:
10: "wanted": [
11: {
12: "found": false,
13: "equation": [
14: {
15: "lhs": {
16: "lhs": {
17: "lhs": {
18: "role": "constant",
19: "symbol": "tip2015/list_assoc.smt2bind",
20: "type": "unknown"
21: },
22: "rhs": {
23: "lhs": {
24: "lhs": {
25: "role": "constant",
26: "symbol": "tip2015/list_assoc.smt2bind",
27: "type": "unknown"
28: },
29: "rhs": {
30: "role": "variable",
31: "type": "(grammars/packrat_unambigPackrat.smt2list a)",
32: "id": 0
33: },
34: "role": "application"
35: },
36: "rhs": {
37: "role": "variable",
38: "type": "(=> a (grammars/packrat_unambigPackrat.smt2list b))",
39: "id": 0
40: },
41: "role": "application"
42: },
43: "role": "application"
44: },
45: "rhs": {
46: "role": "variable",
47: "type": "(=> b (grammars/packrat_unambigPackrat.smt2list c))",
48: "id": 0
49: },
50: "role": "application"
51: },
52: "rhs": {
53: "lhs": {
54: "lhs": {
55: "role": "constant",
56: "symbol": "tip2015/list_assoc.smt2bind",
57: "type": "unknown"
58: },
59: "rhs": {
60: "role": "variable",
61: "type": "(grammars/packrat_unambigPackrat.smt2list a)",
62: "id": 0
63: },
64: "role": "application"
65: },
66: "rhs": {
67: "lhs": {
68: "lhs": {
69: "role": "constant",
70: "symbol": "tip2015/list_assoc.smt2bind",
71: "type": "unknown"
72: },
73: "rhs": {
74: "lhs": {
75: "lhs": {
76: "role": "constant",
77: "symbol": "@",
78: "type": "unknown"
79: },
80: "rhs": {
81: "role": "variable",
82: "type": "(=> a (grammars/packrat_unambigPackrat.smt2list b))",
83: "id": 0
84: },
85: "role": "application"
86: },
87: "rhs": {
88: "role": "variable",
89: "type": "a",
90: "id": 0
91: },
92: "role": "application"
93: },
94: "role": "application"
95: },
96: "rhs": {
97: "role": "variable",
98: "type": "(=> b (grammars/packrat_unambigPackrat.smt2list c))",
99: "id": 0
100: },
101: "role": "application"
102: },
103: "role": "application"
104: },
105: "relation": "~="
106: }
107: ],
108: "file": "tip2015/list_assoc.smt2"
109: }
110: ]
111:
112:
113: This renders to:
114:
115: (tip2015/list_assoc.smt2bind ((tip2015/list_assoc.smt2bind v0) v1)) v2
116: ~= (tip2015/list_assoc.smt2bind v0) ((tip2015/list_assoc.smt2bind ((@
117: v1) v3)) v2)
118:
119: Or, less verbosely:
120:
121: bind (bind v0 v1) v2 ~= bind v0 (bind (@ v1 v3) v2)
122:
123: This seems a little odd: why is there a fully-applied '@'? '@' is
124: function application (equivalent to '$' in Haskell), so '(@ x y)' is
125: equivalent to '(x y)'.
126:
127: We wouldn't expect QuickSpec to find such an equation, for three
128: reasons:
129:
130: - There is no '@' in the signature; the Haskell equivalent is '$'
131: - There is no '$' in the signature, unless we add it (which certainly
132: isn't the case in our benchmarks)
133: - Even if '$' were in the signature, we'd expect to find something like
134: '($) f x ~= f x', and hence congruence closure would throw out any
135: fully-applied '$' calls as redundant.
136:
137: There's something else fishy about this equation too: the
138: right-hand-side contains 'v3', but this doesn't occur on the left.
139: That's OK in general, since information may be thrown away, like in
140: 'const x y = x'. Still, it's unusual to see in a theorem supposedly
141: involving list monads.
142:
143: Digging a little deeper, we look in tip2015/list_assoc.smt2 to find:
144:
145: ; List monad laws
146: (declare-datatypes (a)
147: ((list (nil) (cons (head a) (tail (list a))))))
148: (define-fun-rec
149: (par (a)
150: (append
151: ((x (list a)) (y (list a))) (list a)
152: (match x
153: (case nil y)
154: (case (cons z xs) (cons z (append xs y)))))))
155: (define-fun-rec
156: (par (a b)
157: (bind
158: ((x (list a)) (y (=> a (list b)))) (list b)
159: (match x
160: (case nil (as nil (list b)))
161: (case (cons z xs) (append (@ y z) (bind xs y)))))))
162: (assert-not
163: (par (a b c)
164: (forall ((m (list a)) (f (=> a (list b))) (g (=> b (list c))))
165: (= (bind (bind m f) g)
166: (bind m (lambda ((x a)) (bind (@ f x) g)))))))
167: (check-sat)
168:
169: Notice the theorem statement:
170:
171: (forall ((m (list a)) (f (=> a (list b))) (g (=> b (list c))))
172: (= (bind (bind m f) g)
173: (bind m (lambda ((x a)) (bind (@ f x) g)))))
174:
175: There's a 'lambda' in there! That was somehow discarded during the
176: translation to JSON! It explains where the 'v3' came from (it's the 'x'
177: variable of the 'lambda'). The '@' seems to be an artefact of the TIP
178: format, to make it clear when a variable is being called as a function
179: (I assume this is useful for some translations).
180:
181: What can we do to remedy this situation? The immediate fix seems to be:
182:
183: - If we see 'lambda' in a theorem statement, refuse to spit out an
184: equation. This is quick, avoids having to extend our JSON equation
185: format (for now) and avoids changes to e.g. rendering, congruence
186: closure (which we didn't write!), etc.
187: - If we see '@' fully-applied in a theorem statement, we should
188: simplify it away.
189:
190: We should make a note of this in our writeup, i.e. that not only is
191: QuickSpec limited to equations, it's unable to form new functions
192: (unless the theory contains functions for constructing functions!).
193:
194: The first thing we should do is add regression tests involving 'lambda',
195: '@', etc. to the te-benchmarks code. We should also test what happens
196: with other keywords, like 'match', 'case', etc.
Generated by git2html.