Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- #!/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)))))
- # 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): not (forsome( lambda a: not (p (a))))
- # forsome p = p(find(lambda a: p(a)))
- def forsome(p): p(find_i(lambda a: p(a)))
- def find_i (p):
- if forsome (lambda a: p(zero |q| a)):
- return zero |q| find_i(lambda a: p( zero |q| a))
- else:
- return one |q| find_i(lambda a: p( one |q| a))
- # search p = if forsome(lambda a: p(a)) then Just(find(lambda a: p(a))) else Nothing
- def search (p):
- 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): forevery(lambda a: f(a) == g(a))
- # coerce :: Bit -> Natural
- # coerce Zero = 0
- # coerce One = 1
- coerce = lambda x: x
- # f, g, h :: Cantor -> Integer
- f = lambda a: coerce(a(7 * coerce(a(4)) + 4 * (coerce(a(7))) + 4))
- g = lambda a: coerce(a(coerce(a(4)) + 11 * (coerce(a(7)))))
- def h(a):
- if a(7) == zero:
- if a(4) == zero:
- coerce(a(4))
- else:
- coerce(a( 11))
- else:
- if a(4) == one:
- coerce(a( 15) )
- else:
- coerce(a(8))
- # modulus :: (Cantor -> Integer) -> Natural
- # FIXME
- def modulus (f): least(lambda n: forevery(lambda a: forevery(lambda b: (not (eq(n, a, b))) or (f(a) == f( b)))))
- # least :: (Natural -> Bool) -> Natural
- def least (p):
- if p(0):
- x=0
- else:
- x=1
- x + least(lambda n: p(n+1))
- # eq :: Natural -> Cantor -> Cantor -> Bool
- def eq (n,a,b):
- if (n == 0):
- return True
- else:
- return (a(n-1) == b (n-1)) and (eq(n,a,b))
- # proj :: Natural -> (Cantor -> Integer)
- def proj(i): lambda a: coerce(a(i))
- # find_ii p = if p(Zero # find_ii(lambda a: p(Zero # a)))
- # then Zero # find_ii(lambda a: p(Zero # a))
- # 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))
- equal(f,g)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement