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.
Yes.
> 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
unreadable.
> 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
forms.
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 (http://www.madore.org/~david/programs/unlambda/)
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)
> SII(SI(S(KI)I))
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.
Best,
Bruno
http://iridia.ulb.ac.be/~marchal/
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups "Everything List" group.
To post to this group, send email to everything-list.domain.name.hidden
To unsubscribe from this group, send email to everything-list-unsubscribe.domain.name.hidden
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---
Received on Wed Feb 13 2008 - 09:12:11 PST