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 [EMAIL PROTECTED] To unsubscribe from this group, send email to [EMAIL PROTECTED] For more options, visit this group at http://groups.google.com/group/everything-list?hl=en -~----------~----~----~----~------~----~------~--~---