View file src/colab/ton_explore.py - Download

# -*- coding: utf-8 -*-
"""ton_explore.ipynb

Automatically generated by Colaboratory.

Original file is located at
    https://colab.research.google.com/drive/13q_p7Zjl0fKVnt1DTRyD8Dlxejg3jdUI

Taranovsky Ordinal Notation fundamental sequences in Haskell

Links:
* https://googology.fandom.com/wiki/User_blog:Nayuta_Ito/Introduction_to_Taranovsky%27s_Ordinal_Notation
* https://cs.nyu.edu/pipermail/fom/2012-March/016349.html
* http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm
* http://log.chez.com/text/logic/ordinal_notations.pdf
"""

!apt-get install hugs

# Commented out IPython magic to ensure Python compatibility.
# %%writefile ton_explore.hs
# module Main where
# 
#  import Data.Typeable
# 
#  -- Definition of ordinals in Taranovsky Ordinal Notation
#  data Ton = O | W | C Ton Ton
#   deriving (Eq, Show)
# 
#  -- Item of postfix representation
#  data PostfixItem = CP | OP | WP
#   deriving (Eq, Show, Ord)
# 
#  -- Convert to postscript representation
#  postfix O = [ OP ]
#  postfix W = [ WP ]
#  postfix (C a b) = postfix b ++ postfix a ++ [ CP ]
# 
#  -- short representation of postfix form
#  string_postfix [] = ""
#  string_postfix (CP:l) = "C" ++ string_postfix l
#  string_postfix (OP:l) = "O" ++ string_postfix l
#  string_postfix (WP:l) = "W" ++ string_postfix l
# 
#  -- Compare ordinals by comparing postfix representations
#  instance Ord Ton where
#   compare a b = compare (postfix a) (postfix b)
# 
#  -- List of subterms of an ordinal
#  subterms O = [ O ]
#  subterms W = [ W ]
#  subterms (C a b) = [ C a b ] ++ subterms a ++ subterms b
# 
#  -- nbfbf n a b : a is n-built from below from b
#  nbfbf 0 a b = a <= b                    -- a is O-BFB from b if and only if a           --  for all subterm c of a,
#    c <= a ||                             --   either c <= a
#    flip any (subterms a) (\d ->          --   or there exists subterms d of a such that
#     elem c (subterms d) && nbfbf n d b)) --    c is a subterm of d and d is n-BFB from b
# 
#  -- standard n a : a is in standard form in n-th system
#  standard _ O = True    -- 0 is standard
#  standard _ W = True    -- W is standard
#  standard n (C a b) =   -- C(a,b) is standard if and only if :
#   standard n a &&       --  a is standard
#   standard n b &&       --  b is standard
#   (case b of            --  b is 0 or W or C(c,d) with a <= c
#     O -> True
#     W -> True
#     C c d -> a <= c) &&
#   nbfbf n a (C a b)     -- a is n-BFB from C(a,b)
# 
#  -- list_ton_l l = list of ordinals with l C's in their representation
#  list_ton_l 0 = [ O, W ]
#  list_ton_l k1 = let k = k1-1 in
#   concat (flip map [0..k] (\l ->
#    concat (flip map (list_ton_l l) (\c ->
#     concat (flip map (list_ton_l (k-l)) (\d ->
#      [ C c d ] )) )) ))
# 
#  -- fs n a k = k-th element of fundamental sequence of a in n-th system
#  -- a[k] = max { b | L(b) = k, b is standard and b < a }
#  fs n a k = foldr (\x -> \y -> if (x <= y) then y else x) O
#              (flip filter (list_ton_l k) (\b -> (standard n b) && (b < a)))
# 
#  printfs1 n a i j =
#   if i > j
#   then return True
#   else do
#    putStr ("[" ++ (show i) ++ "] " ++ (show (fs n a i)) ++ "\n")
#    printfs1 n a (i+1) j
#    return True
# 
#  printfs name n a i j = do
#   putStr (name ++ " n=" ++ show n ++ "\n" ++ show a ++ "\n")
#   printfs1 n a i j
#   putStr "\n"
# 
#  -- ccnvert to 0 suc lim
# 
#  ident x = x
# 
#  data On
#   = Zero
#   | Suc On
#   | Lim On (On -> On)
# 
#  intofon Zero = 0
#  intofon (Suc a) = intofon a + 1
# 
#  onofton :: Int -> Ton -> On
#  onofton n O = Zero
#  onofton n W = Lim (Suc Zero) ident
#  onofton n (C O b) = Suc (onofton n b)
#  onofton n (C a b) =
#   Lim Zero (\k -> onofton n (fs n (C a b) (intofon k)))
# 
#  -- main = print (fs 1 (C (C O O) O) 3)
# 
#  main = do
#   printfs "w"     1 (C (C O O) O) 1 3
#   printfs "w.2"   1 (C (C O O) (C (C O O) O)) 1 5
#   printfs "w^2"   1 (C (C O (C O O)) O) 1 6
#   printfs "w^w"   1 (C (C (C O O) O) O) 1 6
#   printfs "e_0"   1 (C W O) 1 6
#   printfs "e_0"   2 (C (C W O) O) 1 6
#   printfs "e_0.2" 1 (C (C W O) (C W O)) 1 6
#   printfs "z_0"   1 (C (C W W) O) 1 6
#   printfs "z_0"   2 (C (C (C W O) (C W O)) O) 1 6
#   printfs "G_0"   1 (C (C (C W W) W) O) 1 6
#   printfs "LVO"   1 (C (C (C (C W W) W) W) O) 1 6
#   printfs "BHO"   2 (C (C W (C W O)) O) 1 6
#   printfs "W_0"   0 W 1 6
#   printfs "W_1"   1 W 1 6
#   printfs "W_1"   2 (C W O) 1 6
#   printfs "W_2"   2 W 1 6
#

!(echo ':load ton_explore'; echo 'main') | hugs