Re: Key Post 1, toward Church Thesis and Lobian machine

From: Bruno Marchal <>
Date: Wed, 13 Feb 2008 15:12:01 +0100

Le 11-févr.-08, à 17:58, Mirek Dobsicek a écrit :

>> "But thanks to that crashing, *Church thesis remains consistent*. I
>> would just say "An existence of a universal language is not ruled
>> out".
>> I am ok with you. Consistent (in math) means basically "not rule out".
>> "Formally consistent" means "not formally ruled out", or "not
>> refutable".
>> That is:
>> "Consistent(p") is the same as "~ Provable(~ p)" " ~" = negation
>> like "Provable(p)" is equivalent with "~ Consistent( ~ p)"
> All right...
> Now, let me just rephrase few points of the key post one more time. I
> will try to be picky with wording. Points which are not mentioned - I
> fill comfortable with.
> 1\ There is no language/algorithm/procedure/machine which can
> describe/execute all total computable functions.

I guess (and have some confirmation below) that you mean here that
there is no language/algorithm/procedure/machine which can
describe/execute all total computable functions AND ONLY TOTAL
COMPUTABLE FUNCTIONS. Right? Otherwise you would be saying that Church
Thesis is false.

> 2\ There exists non-empty set of all machine computable functions
> (inevitably includes both total and strict partial functions). Let us
> call this set MC (machine computable).

OK. (this confirms what I say above).

> 3\ Church himself *defined* the set of
> so-far-known-computable-functions
> as those computable by lambda calculus.

Well, for Church, Lambda does define the set of all computable (total
and partial) functions, not just the so-far-known-comp-functions.

> 4\ What we use to call a *Church thesis* today says, that MC is in fact
> equal to the set of functions computable by lambda calculus.


> 5\ Church thesis is refutable.

Yes. (It is enough to give a function which we can compute, but which
would not be Turing or Lambda computable.

>> * * *
>> Something else:
>> to us verify MM = SII(SII) does crash the system:
>> SII(SII) = I(SII)(I(SII)) = SII(SII) = I(SII)(I(SII)) = SII(SII) =
>> I(SII)(I(SII)) = SII(SII) = I(SII)(I(SII)) = SII(SII) = ...
>> (crashing).
> Working with SK combinators, I had a bit problems with omitted
> parenthesis.

Just avoid writing the left parentheses. SII(SII) is really put for
(((SI)I)((SI)I)) which is conceptually clearer, but practically

> Also it was not clear to me what is the meaning of eg.
> (SKK) since S is expected to take three arguments.

OK, my fault. It means the construct is stable and waiting for more
argument. so SKK, without any added inputs remains SKK and constitutes
a combinator described as being SKK. Such construct are useful for
making data structures for example. Such construct are called normal
The idea is that the 2-variables function Lx Ly (x + y) when applied on
just one argument, 5, say, gives a new function Ly (5 + y), which is a
1-variable function adding 5 to its input. It is the way Schoenfinkel
managed to have only function of one argument.

> What helped me was
> the unlambda language (

At first sight this is just lambda calculus (and thus combinator) with
awkward notation ....

> So here is my crashing sequence (yep, yours is shorter) (I don't expand
> the I term to keep it short)

Good idea. "I" is really a "macro" for "SKK".
I hope everybody see that SKKx = x for any x. SKKx = Kx(Kx) = x. (cf
Sabc = ac(bc); Kab = a)


Hmmm... ok, that's working, but S(KI)I is really I, and you could have
make something simpler ...

> a reference implementation in unlambda:
> ```sii``si``s`kii
> the ` stands for 'apply' operation, aka left parenthesis.

You really need spectacles here ...

> with a small modification
> ```sii``si``s`k.ui
> we can achieve the computer to print uuuuuuuuuuuuu.... in an endless
> loop. .u is a special function with a side effect of printing the
> character u.

You are not supposed to use anything but K and S (or anything you have
already define with K and S) ... I'm not completely sure what you mean
by k.ui (the dot) ... hmm... I see, it prints, well ok then.

I will try to comment your "UDA paper" post asap.



You received this message because you are subscribed to the Google Groups "Everything List" group.
To post to this group, send email to
To unsubscribe from this group, send email to
For more options, visit this group at
Received on Wed Feb 13 2008 - 09:12:11 PST

This archive was generated by hypermail 2.3.0 : Fri Feb 16 2018 - 13:20:14 PST