/
explanation.txt
153 lines (102 loc) · 3.79 KB
/
explanation.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
9 Oct 2016
Explanation:
This example shows Barliman proving that the given partial definition of the "deep" version of 'remove-foo' is incompatible with the test:
(remove-foo '((d foo) foo (e (foo f foo)) foo g foo (h)))
=>
'((d foo) (e (foo f foo)) g (h))
This is because the [(pair? (car ls)) ...] clause is missing from the partial definition. One screenshot shows the test failing, while the other screenshot shows all individual tests passing once the partially-specified clause
[(pair? (car ls)) ,D]
has been added to the partial definition.
Thanks to Michael Adams and Matt Might for an interesting discussion and suggestions that lead to this example. In particular, I believe Michael suggested a test that could detect a missing clause. Matt strongly suggested pushing on the "Refutation-Oriented Programming" angle (a phrase he coined), of which this test is an example.
This example is interesting because:
(1) the partial definition of 'remove-foo' is at least plausible, in that the programmer is writing the lhs first before tackling the rest of the definition---note that the [else (cons (car ls) ,C)] structure is necessary for refutation, since otherwise the 'else' clause could contain a nested conditional;
(2) only the rhs being edited (in the 'else' clause) is instantiated at all
(3) no gensyms are used in the tests;
(4) retutation is fast (about a second).
Code:
The complete definition of "deep" 'remove-foo' is
(define remove-foo
(lambda (ls)
(cond
[(null? ls) '()]
[(pair? (car ls)) (cons (remove-foo (car ls)) (remove-foo (cdr ls)))]
[(equal? (car ls) 'foo) (remove-foo (cdr ls))]
[else (cons (car ls) (remove-foo (cdr ls)))])))
This version of 'remove-foo' works over "deep" lists---that is, it removes any 'foo symbols nested inside a sublist.
The partial definition of 'remove-foo' given in Definitions pane for refutation:
(define remove-foo
(lambda (ls)
(cond
[(null? ls) ,A]
[(equal? (car ls) 'foo) ,B]
[else (cons (car ls) ,C)])))
Adding the partially-instantiated [(pair? (car ls)) ,D] clause allows all the individual tests to pass, but is not sufficient for synthesis of the missing code:
(define remove-foo
(lambda (ls)
(cond
[(null? ls) ,A]
[(pair? (car ls)) ,D]
[(equal? (car ls) 'foo) ,B]
[else (cons (car ls) ,C)])))
Tests:
(remove-foo '())
=>
'()
(remove-foo '(a))
=>
'(a)
(remove-foo '(foo))
=>
'()
(remove-foo '(b foo c))
=>
'(b c)
(remove-foo '(bar foo baz (foo) foo ((quux foo) foo)))
=>
'(bar baz (foo) ((quux foo) foo))
(remove-foo '((d foo) foo (e (foo f foo)) foo g foo (h)))
=>
'((d) (e (f)) g (h))
Setup:
Will's MacBook Pro (Retina, 15-inch, Early 2013)
2.8 GHz Intel Core i7
16 GB 1600 MHz DDR3 RAM
OS X El Capitan 10.11.6
Screenshot was taken on branch conde1-no-deepening, but the main branch now also has the same behavior. Main branch SHA: 700372294d2573231ad14fa2d7803aeae4c1cc82
Set conde1 optimization flag to true in mk/mk.scm:
;; To allow use of experimental `conde1` optimization, set this to #t.
(define enable-conde1? #t)
---------------------------------------------------------
We can use `remove` rather than `remove-foo`:
(define remove
(lambda (x ls)
(cond
[(null? ls) ,A]
[(pair? (car ls)) ,D]
[(equal? (car ls) x) ,B]
[else (cons (car ls) ,C)])))
(define remove
(lambda (x ls)
(cond
[(null? ls) ,A]
[(equal? (car ls) x) ,B]
[else (cons (car ls) ,C)])))
(remove 'foo '())
=>
'()
(remove 'foo '(a))
=>
'(a)
(remove 'foo '(foo))
=>
'()
(remove 'foo '(b foo c))
=>
'(b c)
(remove 'foo '(bar foo baz (foo) foo ((quux foo) foo)))
=>
'(bar baz (foo) ((quux foo) foo))
(remove 'foo '((d foo) foo (e (foo f foo)) foo g foo (h)))
=>
'((d) (e (f)) g (h))
---------------------------------------------------------