View difference between Paste ID: QS7b2N8Q and KMUtKuMJ

 #!/usr/bin/env python
 
 
 # -- File "seemingly-impossible.hs",
 # -- automatically extracted from literate Haskell
 # -- file http://www.cs.bham.ac.uk/~mhe/papers/seemingly-impossible.html
 # --
 # -- Martin Escardo, September 2007
 # -- School of Computer Science, University of Birmingham, UK
 # --
 # -- These algorithms have been published and hence are in the
 # -- public domain.
 # --
 # -- If you use them, I'd like to know! mailto:m.escardo@cs.bham.ac.uk
 #
 # infix hack:
 # https://code.activestate.com/recipes/384122/
 class Infix:
     def __init__(self, function):
         self.function = function
     def __ror__(self, other):
         return Infix(lambda x, self=self, other=other: self.function(other,
 x))
     def __or__(self, other):
         return self.function(other)
     def __rlshift__(self, other):
         return Infix(lambda x, self=self, other=other: self.function(other,
 x))
     def __rshift__(self, other):
         return self.function(other)
     def __call__(self, value1, value2):
         return self.function(value1, value2)
 
 
 def ifthen(test, trueF, falseF):
  if (test):
    return trueF()
  else:
    return falseF()
 
 # data Bit = Zero | One
 #          deriving (Eq)
 
 # Don't bother with a dedicated type or coerce, just define some constants
 zero = 0
 one = 1
 
 
 # type Natural = Integer
 # type Cantor = Natural -> Bit
 # (#) :: Bit -> Cantor -> Cantor
 
 # x # a = lambda i: if i == 0 then x else a(i-1)
-q = Infix ( lambda x, a: (lambda i: ifThen ((i ==0), (lambda: x), (lambda: a(i-1)))))
+def q(x,a): return (lambda i: ifthen ((i ==0), (lambda: x), (lambda: a(i-1))))
 
 # forsome, forevery :: (Cantor -> Bool) -> Bool
 # find :: (Cantor -> Bool) -> Cantor
 # find = find_i
-find = lambda p: find_i(p)
+
 # find_i :: (Cantor -> Bool) -> Cantor
 # find_i p = if forsome(lambda a: p(Zero # a))
 #            then Zero # find_i(lambda a: p(Zero # a))
 #            else One  # find_i(lambda a: p(One  # a))
 # search :: (Cantor -> Bool) -> Maybe Cantor
 
 # forevery p = not(forsome(lambda a: not(p a)))
 def forevery(p): return (not (forsome( lambda a: not (p (a)))))
-def forevery(p): not (forsome( lambda a: not (p (a))))
+
 # forsome p = p(find(lambda a: p(a)))
 def forsome(p): return (p(find_ii(lambda a: p(a))))
-def forsome(p): p(find_i(lambda a: p(a)))
+
 def find_ii(p): return (lambda j: ifthen (p(q (zero, find_ii (lambda a: p(q(zero, a)))))
-def find_i (p):
+         ,lambda : q(zero, find_ii(lambda a: p(q(zero, a))))(j)
-  if forsome (lambda a: p(zero |q| a)):
+         ,lambda : q(one, find_ii(lambda a: p(q(one, a))))(j)))
-    return zero |q| find_i(lambda a: p( zero |q| a))
+
 # search p = if forsome(lambda a: p(a)) then Just(find(lambda a: p(a))) else Nothing
-    return one  |q| find_i(lambda a: p( one  |q| a))
+
  if forsome(lambda a : p(a)):
    find(lambda a: p(a))
  else: None
 
 # equal :: Eq y => (Cantor -> y) -> (Cantor -> y) -> Bool
 # equal f g = forevery(lambda a: f(a) == g(a))
 def equal(f, g): return (forevery(lambda a: f(a) == g(a)))
 
 # coerce :: Bit -> Natural
-def equal(f, g): forevery(lambda a: f(a) == g(a))
+
 # coerce One = 1
 coerce = lambda x: x
 
 # f, g, h :: Cantor -> Integer
 f = lambda a: coerce(a(2 * coerce(a(4)) +  4 * (coerce(a(5)))))
 g = lambda a: coerce(a(coerce(a(4)) + 4 * (coerce(a(5)))))
 def h(a):
-f = lambda a: coerce(a(7 * coerce(a(4)) +  4 * (coerce(a(7))) + 4))
+      if a(5) == zero:
-g = lambda a: coerce(a(coerce(a(4)) + 11 * (coerce(a(7)))))
+
            return (coerce(a(0)))
-      if a(7) == zero:
+
            return (coerce(a(2)))
-           coerce(a(4))
+
            if a(4) == one:
-           coerce(a( 11))
+             return (coerce(a(6) ))
            else:
              return (coerce(a(4)))
-             coerce(a( 15) )
+
 # modulus :: (Cantor -> Integer) -> Natural
-             coerce(a(8))
+
 def modulus (f): return (least(lambda n: forevery(lambda a: forevery(lambda b: (not (eq(n, a, b))) or (f(a) == f( b))))))
 
 # least :: (Natural -> Bool) -> Natural
-def modulus (f):  least(lambda n: forevery(lambda a: forevery(lambda b: (not (eq(n, a, b))) or (f(a) == f( b)))))
+
   if p(0):
    return 0
   else:
    return (1 + least(lambda n: p(n+1)))
-   x=0
+
 # eq :: Natural -> Cantor -> Cantor -> Bool
-   x=1
+
-  x + least(lambda n: p(n+1))
+
     return True
   else:
    return (a(n-1) == b (n-1)) and (eq(n-1,a,b))
 
 # proj :: Natural -> (Cantor -> Integer)
 def proj(i): return (lambda a: coerce(a(i)))
-   return (a(n-1) == b (n-1)) and (eq(n,a,b))
+
 
 # find_ii p = if p(Zero # find_ii(lambda a: p(Zero # a)))
-def proj(i): lambda a: coerce(a(i))
+
 #             else One  # find_ii(lambda a: p(One  # a))
 # find_iii :: (Cantor -> Bool) -> Cantor
 # find_iii p = h # find_iii(lambda a: p(h # a))
 #        where h = if p(Zero # find_iii(lambda a: p(Zero # a))) then Zero else
 #        One
 # find_iv :: (Cantor -> Bool) -> Cantor
 # find_iv p = let leftbranch = Zero # find_iv(lambda a: p(Zero # a))
 #             in if p(leftbranch)
 #                then leftbranch
 #                else One # find_iv(lambda a: p(One # a))
 # find_v :: (Cantor -> Bool) -> Cantor
 # find_v p = lambda n:  if q n (find_v(q n)) then Zero else One
 #  where q n a = p(lambda i: if i < n then find_v p i else if i == n then Zero
 #  else a(i-n-1))
 # find_vi :: (Cantor -> Bool) -> Cantor
 # find_vi p = b
 #  where b = lambda n: if q n (find_vi(q n)) then Zero else One
 #        q n a = p(lambda i: if i < n then b i else if i == n then Zero else
 #        a(i-n-1))
 # find_vii :: (Cantor -> Bool) -> Cantor
 # find_vii p = b
 #  where b = id'(lambda n: if q n (find_vii(q n)) then Zero else One)
 #        q n a = p(lambda i: if i < n then b i else if i == n then Zero else
 #        a(i-n-1))
 
 # data T x = B x (T x) (T x)
 # code :: (Natural -> x) -> T x
 # code f = B (f 0) (code(lambda n: f(2*n+1)))
 #                  (code(lambda n: f(2*n+2)))
 # decode :: T x -> (Natural -> x)
 # decode (B x l r) n |  n == 0    = x
 #                    |  odd n     = decode l ((n-1) `div` 2)
 #                    |  otherwise = decode r ((n-2) `div` 2)
 # id' :: (Natural -> x) -> (Natural -> x)
 # id' = decode.code
 # f',g',h' :: Cantor -> Integer
 # f' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(5^80)) where a' i = coerce(a
 # i)
 # g' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(6^80)) where a' i = coerce(a
 # i)
 # h' a = a' k
 #     where i = if a'(5^80) == 0 then 0    else 1000
 #           j = if a'(3^80) == 1 then 10+i else i
 #           k = if a'(4^80) == 0 then j    else 100+j
 #           a' i = coerce(a i)
 
 # pointwiseand :: [Natural] -> (Cantor -> Bool)
 # pointwiseand [] = lambda b: True
 # FIXME how to emulate pattern match (n:a)
 def  pointwiseand (ns):
   if (ns == []):
     return True
   else:
     return (lambda b: (b(ns[0]) == one) and pointwiseand(ns[0], b))
 
 # sameelements :: [Natural] -> [Natural] -> Bool
 sameelements = lambda a, b:  equal (pointwiseand(a), pointwiseand(b))
 
 print modulus(proj(1))
 print equal(h,h)
 print equal(h,g)
 print equal(h,f)