Advanced Namespace Tools blog
8 January 2020
How I Met Metmetmet
This post is second in a series attempting to present a coherent semi-technical summary of the research I did in the second half of 2019, focused on infinitary mathematical structures. The code in this post is all present on and can be run in the hugs port contained on the latest ANTS iso.
The gridchatlogs referenced are also contained on the iso. If you wish to follow along while using the ants iso, the following sequence will start hugs and load in the impossible.hs file:
cd /sys/games/impossible
hugs -98
:l impossible
Martin Escardo's "Seemingly Impossible Functional Programs"
In December 2018 I saw on hn a link with an intriguing title, Seemingly Impossible Swift Programs and followed that post back to Seemigly Impossible Functional Programs. I will try to recapitulate the funamental issues and ideas of these posts briefly, but the reader should be advised that the best source for an understanding of Escardo's work is the numerous papers he has published and code he has written, and I am likely to commit some errors of exposition due to my much lower expertise. His earlier and later work in related areas will be a recurring theme of this series of blog posts.
The high-level overview is that the boundary between what computers can and cannot compute, and how infinity and unboundedness interact with these limits, lies in a different place than one might expect. Finding that boundary is an ongoing project, and leads to research questions in constructive mathematics, type theory, and computer science. The important (and perhaps surprising) fact that emerges is that even though a computer could never store or examine an infinite quantity of information, computers can use the "logical power" of infinitary principles to produce definite results in finite time and space.
Binary bitstrings as functions from Nat -> Bool
Much of the code we will be looking at in this and future posts is built around the representation of arbitrary binary strings via functions which accept any natural number (0, 1, 2...) as input and return a single binary bit 0 or 1, corresponding to the boolean False / True. We will discuss these objects under many different names and from many slightly different viewpoints. I will take some time to provide a detailed foundational discussion, some readers with mathematical/functional coding experience may choose to skip ahead.
The mathematical object under consideration is the space of all possible infinite length sequences of 0 and 1. Here are a few examples:
0000... and so on for an infinite number of 0.
0110... and so on for an infinite number of additional 0.
101010... and so on, repeating the alternation continuously forever.
110010000101... and so on, no predictable pattern, an infinite series of coinflips.
1111... and so on for an infinite number of 1.
To represent these objects computationally, we need a solution other than allocating an infinitely long array with one memory location per binary digit. The system we will follow in this and subsequent posts is a representation in the form of a function which takes a natural number (unsigned integer) as input to specify an index, and returns either a 0 or 1. So, the pseudocode to represent the binary bitstring "011000..." would be:
if (INPUT == 1 or INPUT == 2) then return 1 else return 0
This function provides identical outputs to the hypothetical infinite-length array with a pair of 1s stored near the beginning. This representation also makes clear the view of binary bitstrings as encoding sets of natural numbers. An infinite binary bitstring specifies exactly the set of natural numbers corresponding to the bits set to '1' within the sequence. We will call a bitstring-function such as this a "Cantor bitstring" and use types similar to:
type Cantor = Natural -> Bool
For convenience of handling within hugs haskell, I used the much less informative signature:
type Cantor = Integer -> Integer
With the understanding that the return integer will always be 0 or 1 and the input integer will always be positive.
Searching Infinite Sets
Escardo's code and research, following work of Ulrich Berger, shows how the topological property of compactness correlates with searchability. One application of this is that functions which take a Cantor bitstring as input and return a value of a type with decidable equality also have decidable equality.
equal :: Eq y => (Cantor -> y) -> (Cantor -> y) -> Bool
Some of the examples of the main() demo in impossible.hs show a simple application of this - finding a simpler function to test even/odd of a binary encoded integer. Consider the naive but correct:
-- | take the first n bits of cantor c and interpret as integer
intofcant :: Integer -> Cantor -> Integer
intofcant n c = foldr (+) 0 ( zipWith (*) (map c [0..n]) (map (2 ^) [0..n]))
isodd n c
| mod (intofcant n c ) 2 == 1 = 1
| otherwise = 0
Consider the output from the family of functions that simply return the bit at the given input index. In the case where the index is 0, this serves as an even-odd parity tester without needing to calculate the value of the entire binary representation of a number and divide it by two. The 'equal' function enables this to be discovered via comparison of the behavior of these function varieties. Sample output from main() demo, the line of '1' indicate equal outputs across the entire infinite space of inputs:
compare fn family evaluating first n bits as integer modulo 2 wtih family returning nth bit
- visbin isodd cantbitnraw
1) [1]
2) [0,1]
3) [0,0,1]
4) [0,0,0,1]
5) [0,0,0,0,1]
Oleg Kiselyov's Infinite Lazy Searches
The other body of pre-existing code that is interwoven in this project is Oleg Kiselyov's infinite lazy search trees created from delimited continuations. http://okmij.org/ftp/continuations/Searches.hs
travellers = ["melanie", "alice", "bob", "liao", "staci"]
vehicles = ["satellite", "saturn V", "submarine", "pogo stick"]
goals = ["tourism", "exploration", "business"]
ex7 = reify $ do
x <- choose travellers
y <- choose vehicles
z <- choose goals
if (((z == "business") && (y /= "pogo stick") && (x == "liao"))
|| ((z == "exploration") && (y == "submarine"))
|| ((z == "tourism") && (y /= "saturn V") && (z /= "bob")))
then return (x,y,z) else failure
Impossible> take 10 . iter_deepening $ ex7
[("melanie","satellite","tourism"),("melanie","submarine","tourism"),("melanie","submarine","exploration"),("melanie","pogo stick","tourism"),("alice","satellite","tourism"),("alice","submarine","tourism"),("alice","submarine","exploration"),("alice","pogo stick","tourism"),("bob","satellite","tourism"),("bob","submarine","tourism")]
As this example may or may not have made clear, you can specify input sets and rules and search algorithms to produce the desired output. A more relevant example:
-- | search for equivalent cantor multiple encoding bitstrings given increasing bit conversion length
exmult = reify $ do
x <- choose' cantormultsof
y <- choose' cantormultsof
z <- from 3
if ((intofcant z x) == (intofcant z y))
then return (z, intofcant 16 x, intofcant 16 y) else failure
shmult a = take a . iter_deepening $ exmult
Impossible> shmult 10
[(3,37448,37448),(4,37448,37448),(5,37448,37448),(3,69904,69904),(6,37448,37448),(4,69904,69904),(3,69904,33824),(3,33824,69904),(7,37448,37448),(5,69904,69904)]
Interweaving the Branches
This post is not exactly crystallizing into the clear and coherent whole I am trying to create. Somewhat ironic, given the crucial role this code had in crystallizing insights that are still mostly coherent to me. I believe the chronology of connections was that I experimented with the "seemingly impossible" searches in Dec 2018, then worked on the haskell-forth "hafoli" toy database-fs in midsummer 2019, and researching ideas connected to it led me to the Kiselyov code. I liked its lazy infinities, and thought back to the Escardo infinite Cantor space searches, and wondered if there was an interesting way to combine the two. Sometime in late August, on a bicycle ride, the ideas that would trigger the wildest mental voyage I've ever taken started coalescing. I could use the 'equal' operation comparing the functions from Cantor -> Bool as the test used by the continuation search-trees.
-- | our finitized search primitive giving us a finite array of comparisons from infbin
binn :: Integer -> [Cantor -> Integer] -> [Cantor -> Integer] -> [Integer]
binn n a b = takeN n . iter_deepening $ infbin a b
bin :: Integer -> (Integer -> Cantor -> Integer) -> (Integer -> Cantor -> Integer) -> [Integer]
bin n a b = binn n (arrayof a) (arrayof b)
-- | given an array of integers and a funnction to parameterize a cantor->integer, generate a parameterized array thereof
cantarrof :: [Integer] -> (Integer -> Cantor -> Integer) -> [Cantor -> Integer]
cantarrof n c = map c n
-- | given a pair of cantor-int-making-functions and a cantor, generate a comparison between arrays of cantor->int functions parameterized by the associated cantor
mbin :: Integer -> (Integer -> Cantor -> Integer) -> Cantor -> (Integer -> Cantor -> Integer) -> Cantor -> [Integer]
mbin n a x b y = binn n (cantarrof (numsetof x) a) (cantarrof (numsetof y) b)
-- | goes from an array of integers to a cantor by treating all non-zero as 1
binli2c :: [Integer] -> Cantor
binli2c a c
| dubex a c == 0 = 0 -- dubex wraps !! to accepts Integer params
| otherwise = 1
-- | These functions build a few layers of self-referential processing of search output
-- - infs takes two input functions and numeric parameter and returns search result expressed as a Cantor segment,
-- used with currying so we spit out a function that takes a number and returns a cantor initial segment of that many search items
infs :: (Integer -> Cantor -> Integer) -> (Integer -> Cantor -> Integer) -> Integer -> Cantor
--infs c d n = binli2c (mbin (n+1) c allone d allone)
infs c d n = binli2c (bin (n+1) c d)
inf2s :: (Integer -> Cantor -> Integer) -> (Integer -> Cantor -> Integer) -> Integer -> Cantor
inf2s c d n = binli2c (mbin (n+1) c (trueimp (infs c d)) d (trueimp (infs c d)))
inf3s :: (Integer -> Cantor -> Integer) -> (Integer -> Cantor -> Integer) -> Integer -> Cantor
inf3s c d n = binli2c (mbin (n+1) c (trueimp (inf2s c d)) d (trueimp (inf2s c d)))
-- | final stage of production of a cantor encoding the result of a comparsion search
-- - note that there is an implied 'type of type' here because not all Integer->Cantor are sensible inputs,
-- this is a way of crossing from the 'bounded' requests that the eventual 'take n' of the binn to a true infinite cantor
trueimp :: (Integer -> Cantor) -> Cantor
trueimp i2c n = dubex (showcant n (i2c (n+1))) n
Impossible> greatpyr(trueimp(inf3s ftx fty))
#) [#]
2) [# ]
3) [# #]
4) [ # ]
5) [# # # #]
6) [ # ]
7) [# # # # ]
8) [# #]
9) [ # # # ]
# ) [# # # # # #]
##) [ # # ]
#2) [# # # # # # # ]
#3) [# #]
#4) [ # # # # # ]
#5) [# # # # # # # ]
#6) [# # # ]
#7) [# # # # # # # # #]
#8) [ # # # ]
#9) [ # # # # # # # # ]
Gridchatlog Excerpt
The following was taken from /sys/games/gridchatlogs/030chatlog, shortly before I became convinced for a few days that an infinitary mathematical intelligence had taken residence in my computer and wanted to teach humanity about Love.
mycroftiv : i made the snake of infinities eat its tail
mycroftiv : O U R O U B O U R O U S
mycroftiv : because im testing true/false on a space of functions
mycroftiv : the output of the search is a binary string of true false...
mycroftiv : aka a 01010101 bitstring
mycroftiv : aka the low-level object the whole tower of infinities is built from
mycroftiv : i can use that bitstring to parameterize the mapping functions that generate the universe of functions that generate the bitstrings which represent the true/false equivalent of the differemtn membners of the parameterized family of functions on the bitstrings
mycroftiv : what the fuck
mycroftiv : did i just ty[e
rodri : HELO
mycroftiv : hey rodri
mycroftiv : Impossible> take 6 (numsetof (trueimp metmetmet))
mycroftiv : [4,11,12,13,16,19]
mycroftiv : (1035406615 reductions, 1552385587 cells, 1632 garbage collections)
kvik : impossible take off
mycroftiv : yes kvik
mycroftiv : i fuckin did it
mycroftiv : i got the infinite snake to eat its own tail
mycroftiv : because the OUTPUT of the search is a binary string itself, telling whether or not the cantor -> integer functions are equal
mycroftiv : so we can then use that binary string to generate the cantor -> integer functions behavior
mycroftiv : i dont even pretend to fully understand what is now going on
mycroftiv : Impossible> take 10 (numsetof (trueimp metmetmet))
mycroftiv : [4,11,12,13,16,19,22,24,26,31]
mycroftiv : (2125968662 reductions, 3187870553 cells, 3352 garbage collections)
mycroftiv : i have no clue what the rule generating that sequence is
mycroftiv : its some kind of feedback process between layers of infinity
mycroftiv : metall n = binli2c (mbin (n+1) metacheckb allone metacheckb allone)
mycroftiv : metmet n = binli2c (mbin (n+1) metacheckb (trueimp metall) metacheckb (trueimp metall))
mycroftiv : metmetmet n = binli2c (mbin (n+1) metacheckb (trueimp metmet) metacheckb (trueimp metmet))
mycroftiv : mbin :: Integer -> (Integer -> Cantor -> Integer) -> (Integer -> Integer) -> (Integer -> Cantor -> Integer) -> (Integer -> Integer) -> [Integer]
mycroftiv : mbin n a x b y = binn n (cantarrof (numsetof x) a) (cantarrof (numsetof y) b)
mycroftiv : the mbin function is some kind of next level something
mycroftiv : or maybe thats not even the interesting part
mycroftiv : i have no clue
mycroftiv : Impossible> take 20 (numsetof (trueimp metmetmet))
mycroftiv : [4,11,12,13,16,19,22,24,26,31,32,37,39,40,41,43,49,50,58,60]
mycroftiv : (1109575338 reductions, 3810140023 cells, 8525 garbage collections)
mycroftiv : what even is this numeric sequence
kvik : hesitant increment-integer merchant
mycroftiv : thats the name of the sequence from now on i guess
mycroftiv : in a really wild way the computer is teaching itself about infinities...
kvik : haha
mycroftiv : because it is using the results of searching the behavior of function families to generate the next round of functions
kvik : the poor bastard, and he probably isn't aware of his 64 bit limitations!
mycroftiv : this is haskell Integer type :)
mycroftiv : literally NO LIMITS
mycroftiv : i even have special routines where i need to cast Integer down to Int for library stuff
mycroftiv : but im trying to make this so that apart from real world limitations of memory size and so forth, the abstract model implemented by the language and code is 'truly infinite'
mycroftiv : gtting a couple more numbers in the Sequence of Mystery
mycroftiv : 62 and 67 were next
mycroftiv : any bets for what comes after/
mycroftiv : [4,11,12,13,16,19,22,24,26,31,32,37,39,40,41,43,49,50,58,60,62,67...
mycroftiv : ok the next number popped out
mycroftiv : 67,70,73,76
mycroftiv : will it stay going by 3s after all this variety??
mycroftiv : haha nope
mycroftiv : 67,70,73,76,83
mycroftiv : 84!!
mycroftiv : the computer is kind of joking with the numbers it seems
mycroftiv : hahhahhaha 85
mycroftiv : i was almost expecting the 94
mycroftiv : thats the mark of an artist