> On 25 Oct 2018, at 08:08, Brent Meeker <[email protected]> wrote:
>
>
>
> On 10/24/2018 9:45 AM, Bruno Marchal wrote:
>> Thomas Pavel wanted that something is identical to itself. In most formal
>> combinator theory x = x is given as an axiom, yet I did not take it.
>> Likewise, the rule: if x = y then y = x is also given, usually, but you can
>> prove it too!
>
> That seems silly since "=" is defined to be reflexive and transitive. I
> assume you're going to allow the inference rule of substituting equals for
> equals.
Yes. (At the metalevel, by the complexity of the behaviour of the finite things
(number, combinators), I might assume Hilbert Spaces, sets and categories, like
in theoretical physics. It does not mean that there is in Hilbert space in the
physical reality, nor that there is a physical reality in the ontology.
It is just funny that we don’t have to assume explicitly x = x, as it is
derivable from the transitive axioms in presence of the rule Kxy = x.
It reflects the fact that we can prove that there is an identity combinators,
once we have S and K only. (And if you have follow the combinator thread, you
know that SKK, SKS, SK<anybird> are all identity combinators.
It is easy to conceive a Turing machine which never erase information, as you
can simulate an erasure by building a copy of the machine with the “erased”
memory. So you have Turing universal system which never erase information, so
you can guess that there are universal combinator base without kestrel (K), nor
any other combinators which would cancel variables.
And, indeed {I, B, C, W} is such a base. Ix = x, without an eliminator like K,
we have to assume the identity bird I. B is the applicator/compositor Bfgx =
f(gx), or Bxyz = x(yz), C is a permuter: Cxyz = xzy, and W is a duplicator Wxy
= xyy.
If you have follow the thread on constant: K is what make possible what Church
will forbidden: eliminate a variable from an expression which does not contain
it. In Church’s original calculus: [x]a makes no sense if x does not occur in
a. K manages that situation, as the elimination of x from a, will be Ka, making
the constant function sending x on a, as Kax = a for all x.
Fitch and Rosser have studied the bigger restriction: no eliminator, nor
duplicator. In this case we do lose the universal Turing ability. It is the BCI
algebra, with only applicators/compositors, permitters and the identity
combinator. Things are completely reversible.
They can be extended by Turing universal extension, with modal operator and
embedded in linear and tensorial algebra, useful for the study of reversible
computing.
I will show that each universal machinery transforms the number structure N
into a partial applicative algebra modelling (simulating, “model” is used in
the logician sense) the combinators.
The combinators are very fine grained, but by the fact that they apply to
combinators freely (when untyped), and the closure for recursion, they go
quickly to high level programming language or computational structure.
Adding linearity and using BCI algebra is still a bit like cheating with
respect to the mind-body problem, as the observable have to be derived in a
precise way from self-reference (notably to benefit from the Gödel-Solovay
splitting of G and G*. G* extends properly G, and G* \ G is the proper theology
(the true but unbelievable (rationally)). There is a surreal part in between
rationalism and irrationalism. Also a non expressible part, a non respectable
part, and mechanism, contrary to a common opinion, is the less reductionist
theory, indeed, it provides a very general notion of persons, and makes it play
the key role at many levels in the making of a reality.
Bruno
>
>>
>> That is very simple, but admittedly subtle, probably more difficult than all
>> the exercises given so far, so don’t worry and feel free to look at the
>> solution. Note that the meta-logic is the usual informal classical logic.
>>
>> Here is the formal theory of combinators: Three rules and two reduction
>> axioms:
>>
>> 1) If x = y and x = z, then y = z
>> 2) If x = y then xz = yz
>> 3) If x = y then zx = zy
>> 4) Kxy = x
>> 5) Sxyz = xz(yz)
>>
>> Exercise(*):
>>
>> a) prove that x = x,
>
> Kxy = x Kxz = x
> Substitute Kxz for x in the first expression.
> Kxy = Kxz
> x = x
>
>
>
>>
>> Hint use 1) and 4).
>>
>> 2) prove that the rule which follows is correct:
>>
>> If x = y then y = x.
>
> If x = y then by substitution for equals x = x
>
> I didn't peek till I did the above, but when I did I'll have to mark you down
> for writing Kxy = y. :-)
>
> Brent
>
>>
>>
>> Bruno
>>
>>
>> (*) Solution (coming from a book by Rosser) below:
>>
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>>
>> 1) x = x
>>
>> Proof:
>>
>> Kxy = y (by 4)
>> Thus we have Kxy = x and Kxy = x, so by “1)” we have that x = x.
>>
>> 2) if x = y then y = x
>>
>> Proof
>>
>> Let us suppose x = y. But by the exercise just above, x = x, so now we have
>> x = y and x = x, so by “1)” again, we have y = x.
>>
>>
>>
>
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
