View source for The program of all programs (code generating code)

'''All programs that can be constructed with a truing machine.''' <br>
'''This page is about the explicit code corresponding to the page: [[A true but useless theory of everything]]''' <br>
Even more explicit an output could look something like this: '''[[Systematic listing of all possible programs]]''' <br>
There are some freedoms in the order one systematically constructs all possible lambda calculus expressions.

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. <br>
Thus I decided to put it here as-is despite it being broken ATM. <br>
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]].

== Aims of for the code ==

* First: '''Construct all untyped lambda calculus expressions''' that are <br>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.''' <br> 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]]. <br> 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. <br>
Interesting meaning non-trivially non-terminating. That is: Creating interesting patterns given some [[natural visualization]]. <br>
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. <br>
But more filtering stacked atop more filtering will unendingly blow up the size of the code. <br>
Thereby increasingly deterring from the '''inherent beauty of the most minimal code''' that does no filtering at all. <br>
So filtering code should thus be kept well separated. <br>
One could even say that the complexity within the mountains of code for filtering out boring uninteresting expressions <br>
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'''. <br>
In case there are arbitrary choices that cannot be avoided point that out conspiciously <br>
(e.g. for later exploration of the other options)

=== Specifically ===

'''Use de-Brujin indices''' as with these there is no need for alpha conversions. <br>
There is another option with the same property that might be preferable in some cases ... <br>
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 …}}

<pre>
{-
 ### 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
-}
</pre>

== Related ==

* '''[[Systematic listing of all possible programs]]'''
* [[A true but useless theory of everything]]
* [[Natural visualization]]
* [[Lambda calculus]]

== External links ==

* [https://en.wikipedia.org/wiki/Undecidable_problem Undecidable problem]

== Non serious ==

* http://de.wikipedia.org/wiki/42_%28Antwort%29
* http://en.wikipedia.org/wiki/Answer_to_the_Ultimate_Question_of_Life,_the_Universe,_and_Everything#Answer_to_the_Ultimate_Question_of_Life.2C_the_Universe_and_Everything_.2842.29