# Chaitin's construction

### From HaskellWiki

(Difference between revisions)

EndreyMark (Talk | contribs) m (I had confused e.g. (exempla gratia) with i.e. (idem esse). Now I have corrected it) |
EndreyMark (Talk | contribs) m (The set of syntactiaclly correct bitstring codings of combinatory logic is exactly both the domain of decoding and range of coding function) |
||

Line 16: | Line 16: | ||

Now, Chaitin's construction will be here | Now, Chaitin's construction will be here | ||

− | :<math>\sum_{p\in \mathrm{ | + | :<math>\sum_{p\in \mathrm{Dom}_\mathrm{dc},\;\mathrm{hnf}\left(\mathrm{dc}\;p\right)} 2^{-\left|p\right|}</math> |

where | where | ||

;<math>\mathrm{hnf}</math> | ;<math>\mathrm{hnf}</math> | ||

Line 24: | Line 24: | ||

;<math>2\!\;^{*}</math> | ;<math>2\!\;^{*}</math> | ||

:should denote the set of all finite bit sequences | :should denote the set of all finite bit sequences | ||

− | ;<math>\mathrm{ | + | ;<math>\mathrm{Dom}_\mathrm{dc}</math> |

− | :should denote the | + | :should denote the set of syntactically correct bit sequences (semantically, they may either terminate or diverge), i.e. the domain of the decoding function, i.e. the range of the coding function |

;“Absolut value” | ;“Absolut value” | ||

:should mean the length of a bit sequence (not [[combinatory logic]] term evaluation!) | :should mean the length of a bit sequence (not [[combinatory logic]] term evaluation!) |

## Revision as of 11:39, 3 August 2006

## Contents |

## 1 Introduction

Wikipedia article on Chaitin's construction, referring to e.g.

- Computing a Glimpse of Randomness (written by Cristian S. Calude, Michael J. Dinneen, and Chi-Kou Shu)
- Omega and why math has no TOEs (Gregory Chaitin).

## 2 Basing it on combinatory logic

Some more direct relatedness to functional programming: we can base Ω on combinatory logic (instead of a Turing machine), see the prefix coding system described in Binary Lambda Calculus and Combinatory Logic (page 20) written by John Tromp:

of course, *c*, *d* are metavariables, and also some other notations are changed slightly.

Now, Chaitin's construction will be here

where

- hnf
- should denote an unary predicate “has normal form” (“terminates”)
- dc
- should mean an operator “decode” (a function from finite bit sequences to combinatory logic terms)
- should denote the set of all finite bit sequences
- Dom
_{dc} - should denote the set of syntactically correct bit sequences (semantically, they may either terminate or diverge), i.e. the domain of the decoding function, i.e. the range of the coding function
- “Absolut value”
- should mean the length of a bit sequence (not combinatory logic term evaluation!)

Here, dc is a partial function (from finite bit sequences). If this is confusing or annoying, then we can choose a more Haskell-like approach, making dc a total function:

dc :: [Bit] -> Maybe CL

then, Chaitin's construction will be

where should denote false truth value.