The program of all programs (code generating code)
From apm
Revision as of 10:44, 11 June 2023 by Apm (Talk | contribs) (moved the lssting of nanual cretaed lamda calc expressions out to page Systematic listing of all possible programs & some cleanup)
All programs that can be constructed with a truing machine.
This page is about the explicit code corresponding to the page: A true but useless theory of everything
As it is this Haskell code (see bottom) is ...
- incomplete
- not yet working
- most likely far from the most elegant and (readably) terse approach (that would be highly desirable here)
... but the code should give enough context to put together a working version.
Thus I decided to put it here as-is despite it being broken ATM.
Evetually I'll get back at it to fix it.
Note that much of the code is just a simple implementation of untyped lambda calculus.
Contents
Aims of for the code
- First: Construct all untyped lambda calculus expressions that are
constructible by exhaustive combinatory permutations of continuously increasing size. (Kinda like construction of "the library of babel of code".) - Then: Execute all these untyped lambda calculus expressions
But: Do all this doubly cantor diagonally such that:
- reaching execution of any of the expressions happens in a finite number of computing steps
- every expression starts evaluating in a finite number of computing steps
Then do something more or less interesting with it. This might be:
- Present it in the shortest most elegant way possible.
Ideally T-shirt printable with headline "True Theory of Everything (but useless)" - Determine Chaitins uncomputabe constant Omega (the first digits of ) for this specific "machine"
- Look for non-trivially non-terminating expressions that lead to interesting patterns given some natural visualization.
There are issues with that though.
Issues with looking for interesting expressions within
The execution of this "program of all programs" will most likely take waaay to long to get up to anything interesting.
Interesting meaning non-trivially non-terminating. That is: Creating interesting patterns given some natural visualization.
E.g.: Novel not yet known types of beautiful fractal patterns.
Of course it is possible to try to filter out all the obviously non-interesting cases.
But more filtering stacked atop more filtering will unendingly blow up the size of the code.
Thereby increasingly deterring from the inherent beauty of the most minimal code that does no filtering at all.
So filtering code should thus be kept well separated.
One could even say that the complexity within the mountains of code for filtering out boring uninteresting expressions
has a correspondence to something something (??).
- ... some notion for the degree of inefficiency in generating some notion of interetsingness
- ... the complexity of direct specification of expressions of some notion of interetsingness
This is all rather wishy washy, I know.
Implementation details / design decisions
Generally
With all coding design decisions stick to the most natural self suggesting choice.
In case there are arbitrary choices that cannot be avoided point that out conspiciously
(e.g. for later exploration of the other options)
Specifically
Use de-Brujin indices as with these there is no need for alpha conversions.
There is another option with the same property that might be preferable in some cases ...
See: Lambda calculus
Manual systematic exhaustive code construction
See page: Systematic listing of all possible programs
An attempt in coding this in Haskell (not working yet)
(TODO: Cean up this code & get it working …)
{-
### Lukas Süss 2013
### Lambda Calculus implemented with De Bruijn indices.
http://en.wikipedia.org/wiki/De_Bruijn_index
The use of these indices avoids the necessity of alpha conversions
thus this representation provides the most elegant way to study the complex
beahaviour of the smallest possible programs (possibly leading to new insights into logic)
---------------------------------------------
The plan is to systematically** build all possible programs (since lanbda calculus is turing complete)
and then execute them all in a quasiparallel fashion (** or randomly to look a bit deeper in the possibility space)
The output may later be represented graphically as 2D images and lead to interesting patterns.
One might look especially for the expressions which do not terminate or cycle for a loong time
linechange = evaluation step
hue <-> assoziativity layer
brightness <-> index number
It's easy on paper but pretty big as a program - the code is probably still reducable a lot
-- STILL NO SUCCESS -- FURTHER DEBUGGING EVAL STEP
-- TODO next
further debug evalstep
create cantorized randomlambdaexpressionstream
http://de.wikipedia.org/wiki/Weltformel
http://en.wikipedia.org/wiki/Theory_of_everything
http://de.wikipedia.org/wiki/Chaitinsche_Konstante
what is this machines omega?
minimale definitionsfreiheiten hier
-}
-- import Control.Applicative
import Data.List (nub,delete)
import Debug.Trace
--tracee a = trace (show a) a -- for debugging
tracee a = a
--data Terminat = Halt | Loop Integer | Unknown
-- Brac ... makes the necessary associativity adjustment possible
-- BInd ... De Brujin Index
data Expr = BInd Integer | Brac [Expr] | Lmbd [Expr] -- minimal representation as a tree
-- in de Brujins original paper constants where used too but they are not necessary for turing completeness thus omitted
-- (λ1(λ1(λ1)))(λ21) == (λ1λ1λ1)(λ21) == \z.(\y.y(\x.x)(\x.zx)
example1 = Brac [Lmbd[BInd 1,Lmbd[BInd 1,Lmbd[BInd 1]]],Lmbd[BInd 2,BInd 1]]
-- (λ(λ42(λ13)))(λ51) == (λλ42(λ13))(λ51) == ...
example2 = Brac [Lmbd[Lmbd[BInd 4,BInd 2,Lmbd[BInd 1,BInd 3]]],Lmbd[BInd 5,BInd 1]]
-- try combinatorial build bottom up with lambda extendors
{-
This works :)
*Main> shiftExpr (-1) 0 $ Lmbd[BInd 1,Lmbd[BInd 2,Lmbd[BInd 1]]]
λ[1,λ[2,λ[1]]]
*Main> shiftExpr (-1) 0 $ Lmbd[BInd 2,Lmbd[BInd 2,Lmbd[BInd 1]]]
λ[1,λ[2,λ[1]]]
*Main> example1
[λ[1,λ[1,λ[1]]],λ[2,1]]
*Main> eval1 example1 <<<<<<<<<<<<<<<<<< ERROR: first unevaluatable lambda is evaluated
[λ[2,1],λ[λ[3,1],λ[1]]] <<<<<<<<<< only indices that hit the uppermost lambda have to be suibstituted!!
λz. (λy. y (λx. x)) (λx. z x)
λz. ((λx. x)) (λx. z x)
*Main> Lmbd[BInd 1,Lmbd[BInd 1,Lmbd[BInd 1]]]
λ[1,λ[1,λ[1]]]
*Main> eval1 $ Lmbd[BInd 1,Lmbd[BInd 1,Lmbd[BInd 1]]] <<<<<<<<< ERROR of unknown cause
λ[1,1,1]
*Main> shiftExpr (-1) 0 $ Lmbd[BInd 1,Lmbd[BInd 2,Lmbd[BInd 1]]] -- ok
λ[1,λ[2,λ[1]]]
*Main> shiftExpr (-1) 0 $ Lmbd[BInd 2,Lmbd[BInd 2,Lmbd[BInd 1]]] -- not ok yλ WHY??
λ[1,λ[2,λ[1]]]
-}
{- | eval1 executes one normal order beta evaluation step.
0a) strip expression from top level "right associative bracket" or "lambda bracket" since
the top level expression can never be evaluated
0b) go down to the first evaluatable lambda with bound variables** and argument. call substitution. **bond to top lambda
1) Remove the element which will be used for substitution from behind the lambda.
2) The topmost lambda will be used up so all its bond indices become more unbond - they'll be Decrease by one.
3) Find the topmost lambdas effective binding places.
4) when inserting the argument at the bonding places the indices become more bond - they'll be Increased by their new bondedness.
5) possible: compress free variables (not implemented)
-}
-- | step 0a
eval1 :: Expr -> Expr
eval1 lmbd = case lmbd of
(BInd i) -> BInd i
(Brac expr) -> Brac $ evalList expr
(Lmbd expr) -> Lmbd $ evalList expr
where
evalList :: [Expr] -> [Expr] -- step 0b,1,2
evalList expr = case expr of
[] -> [] -- actually this "atom" list artefact extends lamda calculus in some way (disallow?)
((BInd i) :[]) -> BInd i : []
((BInd i) :es) -> tracee $ BInd i : evalList es
((Brac es'):[]) -> Brac es' : []
((Brac es'):es) -> Brac es' : evalList es
((Lmbd lmbd):[]) -> evalList lmbd -- just one big lambda -> look inside (prevent head [])
((Lmbd lmbd):arg:es) -> if tracee (hasboundvars lmbd) -- only evaluatable when lmbd has bond variables
then (evalList' 0 (strippedLmbd lmbd) arg) ++ es -- (1) eval; reconstruct left assoc. & omit used up argument.
else (Lmbd lmbd) : evalList (arg : es) -- leave unevaluable lambda be and try next (argument becomes new lambda)
where --(keep where for splittability)
strippedLmbd e1 = (shiftList (-1) 0 e1) -- (2)
evalList' :: Integer -> [Expr] -> Expr -> [Expr] -- tracked level -> lambda subexpression -> argument -> result
evalList' level expr arg = case expr of -- first call is always with Lmbd
((BInd i):es) ->
if i == level -- (3)
then (shiftExpr level 0 arg) : (evalList' level es arg) -- (4)
else BInd i : evalList' level es arg -- ?????
[] -> []
((Lmbd e):es) -> evalLevelFor Lmbd e 1 es
((Brac e):es) -> evalLevelFor Brac e 0 es
where evalLevelFor exprType e shift es = (exprType $ evalList' (level+shift) e arg) : evalList' level es arg
--dysfunctional does nonsense -- assert (shift >= (-1))
shiftExpr :: Integer -> Integer -> Expr -> Expr --strip from top expression
shiftExpr shift level expr = case expr of
(Lmbd es) -> Lmbd $ shiftList shift (level+1) es
(Brac es) -> Brac $ shiftList shift level es
(BInd i) -> BInd $ if (i > level) then (i+shift) else i -- seems correct now
shiftList :: Integer -> Integer -> [Expr] -> [Expr] -- describe meaning of arguments
shiftList shift level expr = case expr of
[] -> []
((Lmbd e):es) -> (Lmbd $ shiftList shift (level+1) e) : shiftList shift level es
((Brac e):es) -> (Brac $ shiftList shift level e) : shiftList shift level es
((BInd i):es) -> (shiftExpr shift level (BInd i)) : shiftList shift level es
hasboundvars :: [Expr] -> Bool
hasboundvars expr = hasboundvars' 0 expr
where -- (hasboundvars [Lmbd [BInd 1]] == True)
hasboundvars' :: Integer -> [Expr] -> Bool
hasboundvars' level expr = case expr of
((Lmbd e):es) -> hasboundvars' (level+1) e || hasboundvars' level es
((Brac e):es) -> hasboundvars' (tracee level) e || hasboundvars' level es
((BInd i):es) -> i <= level || hasboundvars' level es -- True if bound
[] -> False
instance Show Expr where
show = showStyle1
-- for some reason showStyles only display unicode when used to define show instances
showStyle1 expr = case expr of
(BInd i) -> show i
(Brac exprs@(e:es)) -> show exprs
(Lmbd exprs@(e:es)) -> "λ" ++ show exprs
(Brac []) -> ""
(Lmbd []) -> ""
-- style2 not woking yet - why get lambdas only displayed when made instance of show?
showStyle2 expr = case expr of
(BInd i) -> show i
(Brac exprs@(e1:e2:es)) -> "(" ++ showStyle2 e1 ++ concatMap showStyle2 (tail exprs)
(Lmbd exprs@(e1:e2:es)) -> "(λ" ++ showStyle2 e1 ++ concatMap showStyle2 (tail exprs)
(Brac (e:[])) -> showStyle2 e ++ ")"
(Lmbd (e:[])) -> showStyle2 e ++ ")"
--Style3: if last element of list give $ option for bracketing to lower level
-- only on finite data
--liftA2 (++) [[1,2],[3,4]] [[5,6],[7,8]] ... [[1,2,5,6],[1,2,7,8],[3,4,5,6],[3,4,7,8]]
-- how to cantorize a tree?? <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
{-
-- | systematically creates every conceivable lambda expression
allLmbds :: Expr]
allLmbds = map Brac (allLmbds' allBInds)
where
allLmbds' :: [[Expr]] -> [[Expr]]
allLmbds' expr =
[is, si, ls (allLmbds' expr), sl (allLmbds' expr), bs (allLmbds' expr), sb (allLmbds' expr)]
where
is = allBInds ++ expr
si = expr ++ allBInds
ls i = [Lmbd i] ++ expr
sl i = seed ++ [Lmbd i]
bs i = [Brac i] ++ expr
sb i = expr ++ [Brac i]
-- how to do this right ????
-}
-- | all possible sequences of de Bruijn Indices
-- allBInds = (map (map BInd) comboStream) -- [[Expr]]
-- | systematic enumeration of discrete infinite dimensional positive space
comboStream :: [[Int]] -- may be useful in general
comboStream = concatMap eqPerms $ orderedComboStream
-- | permutations -- this handles duplicates correctly (unlike Data.List.permutations)
eqPerms [] = [[]] -- thanks to: http://www.mail-archive.com/haskell-cafe@haskell.org/msg49367.html
eqPerms xs = [x:xt | x <- nub xs, xt <- eqPerms $ delete x xs]
-- | all unpermuted number combinations of all lengths (created in cantor style)
orderedComboStream = concatMap orderedCombos [1..] -- [[Int]]
-- | one cantor diagonal
orderedCombos layer = concat [ numCombos (l) (layer-l) | l<-[1..layer-1] ]
-- | one canor element already has multiple subelements
numCombos :: Int -> Int -> [[Int]]
numCombos listlength topnum = map (topnum :) $ numCombos' (listlength-1) topnum
where
numCombos' :: Int -> Int -> [[Int]]
numCombos' listlength topnum =
if (listlength == 0) then [[]] else concat [ map ((topnum - n) :) (numCombos' (listlength-1) (topnum-n)) | n<-[0..(topnum-1)] ]
{-
runEvals lambda = iterate eval1 lambda -- loop checking is nontrivial !
looplength xs = length $ dropWhile (last xs /=) xs -- inefficient (-1?)
instance Read Lambda where .....
getFreeVars :: Lambda -> [Integer])
A variable n is bound if it is in the scope of at least n binders (λ); otherwise it is free
instance Eq Lambda where
(==) a b = .... maybe non terminating function - possibly acceptable in lazy or parallel computations
-- use never without a timeout / cleanup
-- for detection of trivial loops an detection an other behaviour is desired
there are also permutation based approaches for nameless (normal form) representations
-}
{-
-- nonterminatingTruism as = iterate (take 2) as == repeat as
TODO
* check if shift does correct for arounf 0&1 freeness
* check if branching is missing PROBABLY OK NOW was seriously flawed
* add reader instance (spaces)
* build all combinations from basic lambda extension steps -- randomLambdaGenerator ...
add on left or right a LEFT or RIGHT i with or without right side overriding assoziative bracket
>> All programs of the world in one program
>> add notes on connection to chaitins noncomputable Omega
maybe the most fundamental puzzle there is
minimize the use of () by adding $'s ??
* filter for progams which run past a threthhold of evalsteps bevfore terminating
(nontermination of the long running programs is proovable unprovable in general.
how to find and collect such proofs then - heuristics)
hard to catch trivial nonterminating cases:
substring multiplier loop a x -> a a x -> a a a x
extender loop a x -> a a x -> a a a a x
* encoding of: (very hard task: can those be found - probably some interpretation needed ...)
thue-morse sequence
binary squareroot
only recursions on growing parts can lead to nonrepetitive behaviour
OT:
can lamnbacalc be adapted to be a board game (educational)
one evalstep per zug?
can this harsh form be represented in a more visually obvious one (yes: crossing strings to the right)
-}
take2D n m = take n . map (take m)
take3D n m l = take l . map (take m) . map (map (take n))
--takeND ns = compositionate $ zipWith ($) maptowers (map take ns)
-- this is impossible due to emerging infinite types
-- :t ((+1).(+1)) -- doable with foldr1 ??
{-
notes to keep:
wrapperconstructos can't be ommited via use of "type" since cycles in type synonym declarations are not allowed
-}
