Difference between revisions of "Chaitin's construction"
Jump to navigation
Jump to search
EndreyMark (talk | contribs) m (Some rephrasing) |
EndreyMark (talk | contribs) m (I had confused e.g. (exempla gratia) with i.e. (idem esse). Now I have corrected it) |
||
Line 25: | Line 25: | ||
:should denote the set of all finite bit sequences |
:should denote the set of all finite bit sequences |
||
;<math>\mathrm{Rng}_\mathrm{dc}</math> |
;<math>\mathrm{Rng}_\mathrm{dc}</math> |
||
− | :should denote the range of decoding function, |
+ | :should denote the range of decoding function, i.e. the syntactically correct bit sequences (semantically, they may either terminate or diverge), |
;“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:28, 3 August 2006
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).
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, , are metavariables, and also some other notations are changed slightly.
Now, Chaitin's construction will be here
where
- should denote an unary predicate “has normal form” (“terminates”)
- should mean an operator “decode” (a function from finite bit sequences to combinatory logic terms)
- should denote the set of all finite bit sequences
- should denote the range of decoding function, i.e. the syntactically correct bit sequences (semantically, they may either terminate or diverge),
- “Absolut value”
- should mean the length of a bit sequence (not combinatory logic term evaluation!)
Here, is a partial function (from finite bit sequences). If this is confusing or annoying, then we can choose a more Haskell-like approach, making a total function:
dc :: [Bit] -> Maybe CL
then, Chaitin's construction will be
where should denote false truth value.