SHOW:
|
|
- or go back to the newest paste.
1 | #!/usr/bin/env python | |
2 | ||
3 | ||
4 | # -- File "seemingly-impossible.hs", | |
5 | # -- automatically extracted from literate Haskell | |
6 | # -- file http://www.cs.bham.ac.uk/~mhe/papers/seemingly-impossible.html | |
7 | # -- | |
8 | # -- Martin Escardo, September 2007 | |
9 | # -- School of Computer Science, University of Birmingham, UK | |
10 | # -- | |
11 | # -- These algorithms have been published and hence are in the | |
12 | # -- public domain. | |
13 | # -- | |
14 | # -- If you use them, I'd like to know! mailto:m.escardo@cs.bham.ac.uk | |
15 | # | |
16 | # infix hack: | |
17 | # https://code.activestate.com/recipes/384122/ | |
18 | class Infix: | |
19 | def __init__(self, function): | |
20 | self.function = function | |
21 | def __ror__(self, other): | |
22 | return Infix(lambda x, self=self, other=other: self.function(other, | |
23 | x)) | |
24 | def __or__(self, other): | |
25 | return self.function(other) | |
26 | def __rlshift__(self, other): | |
27 | return Infix(lambda x, self=self, other=other: self.function(other, | |
28 | x)) | |
29 | def __rshift__(self, other): | |
30 | return self.function(other) | |
31 | def __call__(self, value1, value2): | |
32 | return self.function(value1, value2) | |
33 | ||
34 | ||
35 | def ifthen(test, trueF, falseF): | |
36 | if (test): | |
37 | return trueF() | |
38 | else: | |
39 | return falseF() | |
40 | ||
41 | # data Bit = Zero | One | |
42 | # deriving (Eq) | |
43 | ||
44 | # Don't bother with a dedicated type or coerce, just define some constants | |
45 | zero = 0 | |
46 | one = 1 | |
47 | ||
48 | ||
49 | # type Natural = Integer | |
50 | # type Cantor = Natural -> Bit | |
51 | # (#) :: Bit -> Cantor -> Cantor | |
52 | ||
53 | # x # a = lambda i: if i == 0 then x else a(i-1) | |
54 | def q(x,a): return (lambda i: ifthen ((i ==0), (lambda: x), (lambda: a(i-1)))) | |
55 | ||
56 | # forsome, forevery :: (Cantor -> Bool) -> Bool | |
57 | # find :: (Cantor -> Bool) -> Cantor | |
58 | # find = find_i | |
59 | ||
60 | # find_i :: (Cantor -> Bool) -> Cantor | |
61 | # find_i p = if forsome(lambda a: p(Zero # a)) | |
62 | # then Zero # find_i(lambda a: p(Zero # a)) | |
63 | # else One # find_i(lambda a: p(One # a)) | |
64 | # search :: (Cantor -> Bool) -> Maybe Cantor | |
65 | ||
66 | # forevery p = not(forsome(lambda a: not(p a))) | |
67 | def forevery(p): return (not (forsome( lambda a: not (p (a))))) | |
68 | ||
69 | # forsome p = p(find(lambda a: p(a))) | |
70 | def forsome(p): return (p(find_ii(lambda a: p(a)))) | |
71 | ||
72 | - | def find_ii(p): return (lambda j: ifthen (p(q (zero, find_ii (lambda a: p(q(zero, a))))) |
72 | + | def find_ii(p): return (ifthen (p(q (zero, lambda j: find_ii (lambda a: p(q(zero, a)))(j))) |
73 | - | ,lambda : q(zero, find_ii(lambda a: p(q(zero, a))))(j) |
73 | + | ,lambda : q(zero, lambda j: find_ii(lambda a: p(q(zero, a)))(j)) |
74 | - | ,lambda : q(one, find_ii(lambda a: p(q(one, a))))(j))) |
74 | + | ,lambda : q(one, lambda j: find_ii(lambda a: p(q(one, a)))(j)))) |
75 | ||
76 | # search p = if forsome(lambda a: p(a)) then Just(find(lambda a: p(a))) else Nothing | |
77 | def search (p): | |
78 | if forsome(lambda a : p(a)): | |
79 | find(lambda a: p(a)) | |
80 | else: None | |
81 | ||
82 | # equal :: Eq y => (Cantor -> y) -> (Cantor -> y) -> Bool | |
83 | # equal f g = forevery(lambda a: f(a) == g(a)) | |
84 | def equal(f, g): return (forevery(lambda a: f(a) == g(a))) | |
85 | ||
86 | # coerce :: Bit -> Natural | |
87 | # coerce Zero = 0 | |
88 | # coerce One = 1 | |
89 | coerce = lambda x: x | |
90 | ||
91 | # f, g, h :: Cantor -> Integer | |
92 | f = lambda a: coerce(a(2 * coerce(a(4)) + 4 * (coerce(a(5))))) | |
93 | g = lambda a: coerce(a(coerce(a(4)) + 4 * (coerce(a(5))))) | |
94 | def h(a): | |
95 | if a(5) == zero: | |
96 | if a(4) == zero: | |
97 | return (coerce(a(0))) | |
98 | else: | |
99 | return (coerce(a(2))) | |
100 | else: | |
101 | if a(4) == one: | |
102 | return (coerce(a(6) )) | |
103 | else: | |
104 | return (coerce(a(4))) | |
105 | ||
106 | # modulus :: (Cantor -> Integer) -> Natural | |
107 | # FIXME | |
108 | def modulus (f): return (least(lambda n: forevery(lambda a: forevery(lambda b: (not (eq(n, a, b))) or (f(a) == f( b)))))) | |
109 | ||
110 | # least :: (Natural -> Bool) -> Natural | |
111 | def least (p): | |
112 | if p(0): | |
113 | return 0 | |
114 | else: | |
115 | return (1 + least(lambda n: p(n+1))) | |
116 | ||
117 | # eq :: Natural -> Cantor -> Cantor -> Bool | |
118 | def eq (n,a,b): | |
119 | if (n == 0): | |
120 | return True | |
121 | else: | |
122 | return (a(n-1) == b (n-1)) and (eq(n-1,a,b)) | |
123 | ||
124 | # proj :: Natural -> (Cantor -> Integer) | |
125 | def proj(i): return (lambda a: coerce(a(i))) | |
126 | ||
127 | ||
128 | # find_ii p = if p(Zero # find_ii(lambda a: p(Zero # a))) | |
129 | # then Zero # find_ii(lambda a: p(Zero # a)) | |
130 | # else One # find_ii(lambda a: p(One # a)) | |
131 | # find_iii :: (Cantor -> Bool) -> Cantor | |
132 | # find_iii p = h # find_iii(lambda a: p(h # a)) | |
133 | # where h = if p(Zero # find_iii(lambda a: p(Zero # a))) then Zero else | |
134 | # One | |
135 | # find_iv :: (Cantor -> Bool) -> Cantor | |
136 | # find_iv p = let leftbranch = Zero # find_iv(lambda a: p(Zero # a)) | |
137 | # in if p(leftbranch) | |
138 | # then leftbranch | |
139 | # else One # find_iv(lambda a: p(One # a)) | |
140 | # find_v :: (Cantor -> Bool) -> Cantor | |
141 | # find_v p = lambda n: if q n (find_v(q n)) then Zero else One | |
142 | # where q n a = p(lambda i: if i < n then find_v p i else if i == n then Zero | |
143 | # else a(i-n-1)) | |
144 | # find_vi :: (Cantor -> Bool) -> Cantor | |
145 | # find_vi p = b | |
146 | # where b = lambda n: if q n (find_vi(q n)) then Zero else One | |
147 | # q n a = p(lambda i: if i < n then b i else if i == n then Zero else | |
148 | # a(i-n-1)) | |
149 | # find_vii :: (Cantor -> Bool) -> Cantor | |
150 | # find_vii p = b | |
151 | # where b = id'(lambda n: if q n (find_vii(q n)) then Zero else One) | |
152 | # q n a = p(lambda i: if i < n then b i else if i == n then Zero else | |
153 | # a(i-n-1)) | |
154 | ||
155 | # data T x = B x (T x) (T x) | |
156 | # code :: (Natural -> x) -> T x | |
157 | # code f = B (f 0) (code(lambda n: f(2*n+1))) | |
158 | # (code(lambda n: f(2*n+2))) | |
159 | # decode :: T x -> (Natural -> x) | |
160 | # decode (B x l r) n | n == 0 = x | |
161 | # | odd n = decode l ((n-1) `div` 2) | |
162 | # | otherwise = decode r ((n-2) `div` 2) | |
163 | # id' :: (Natural -> x) -> (Natural -> x) | |
164 | # id' = decode.code | |
165 | # f',g',h' :: Cantor -> Integer | |
166 | # f' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(5^80)) where a' i = coerce(a | |
167 | # i) | |
168 | # g' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(6^80)) where a' i = coerce(a | |
169 | # i) | |
170 | # h' a = a' k | |
171 | # where i = if a'(5^80) == 0 then 0 else 1000 | |
172 | # j = if a'(3^80) == 1 then 10+i else i | |
173 | # k = if a'(4^80) == 0 then j else 100+j | |
174 | # a' i = coerce(a i) | |
175 | ||
176 | # pointwiseand :: [Natural] -> (Cantor -> Bool) | |
177 | # pointwiseand [] = lambda b: True | |
178 | # FIXME how to emulate pattern match (n:a) | |
179 | def pointwiseand (ns): | |
180 | if (ns == []): | |
181 | return True | |
182 | else: | |
183 | return (lambda b: (b(ns[0]) == one) and pointwiseand(ns[0], b)) | |
184 | ||
185 | # sameelements :: [Natural] -> [Natural] -> Bool | |
186 | sameelements = lambda a, b: equal (pointwiseand(a), pointwiseand(b)) | |
187 | ||
188 | - | print modulus(proj(1)) |
188 | + | print modulus(proj(2)) |
189 | print equal(h,h) | |
190 | print equal(h,g) | |
191 | print equal(h,f) |