Re: Combinator joker (a note in passing on formal combinator theory)
Just a typo error correction I hope you have spotted it > On 24 Oct 2018, at 18:45, 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 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, > > Hint use 1) and 4). > > 2) prove that the rule which follows is correct: > > If x = y then y = x. > > > Bruno > > > (*) Solution (coming from a book by Rosser) below: > > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > ; > > 1) x = x > > Proof: > > Kxy = y (by 4) Kxy = x. (Of course) > 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 everything-list+unsubscr...@googlegroups.com. > To post to this group, send email to everything-list@googlegroups.com. > Visit this group at https://groups.google.com/group/everything-list. > For more options, visit https://groups.google.com/d/optout. -- 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 everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
Re: Combinator joker (a note in passing on formal combinator theory)
> On 24 Oct 2018, at 23:02, Tomas Pales wrote:
>
> Well, you must assume the principle of identity at the beginning,
The logical point is that we can assume something more general the projection
(x y) —> x, which is what the combinator K does.
At the meta intuitive level, I assume such more thing, but when making the
point technical, the devil is in the detail.
In all reversible algebra, identity has to be assume, but allowing (non
reversible) projection make the transitive axiom sufficient; we get the
reflexivity and the symmetry as a gift.
> otherwise all your other assumptions will be their own negations.
At the meta-level, yes. In the formal theory, it happens you can derive it from
projection and transitivity.
That is already true with the axioms of the SK-combinators:
Kxy = x
Sxyz = xz(yz)
But without elimination (like K eliminate y), we need to assume the identity
combinators.
We can add, in the formal theory, the axiom S ≠ K, to avoid having only one
bird, the identity bird. Indeed, we have trivially
III = I
= II(II)
So that {I} is a trivial combinatory algebra. It plays the role of a
contradiction in an equality theory.
Nevertheless a L_obian combinator will have to believe in first order logical
specification, and have the ability to make induction on all combinators.
An ontology without induction can be Turing universal, and allow “creature”
believing in induction, and to extract physics from self-reference (as we have
to for soling the mechanist mind-latter problem) we interview machines
believing in the induction axioms (the self-referentially correct one obeys to
G and G*, from which the logic of the observable is derived. It makes
(classical) computationalism testable.
Bruno
>
> --
> 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 everything-list+unsubscr...@googlegroups.com
> .
> To post to this group, send email to everything-list@googlegroups.com
> .
> Visit this group at https://groups.google.com/group/everything-list
> .
> For more options, visit https://groups.google.com/d/optout
> .
--
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
Re: Combinator joker (a note in passing on formal combinator theory)
> On 25 Oct 2018, at 08:08, Brent Meeker 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 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:
>>
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
>> ;
Re: Combinator joker (a note in passing on formal combinator theory)
> On 24 Oct 2018, at 18:45, Bruno Marchal wrote: > > Thomas Pavel Oops. Thomas Pales. Sorry! > 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 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, > > Hint use 1) and 4). > > 2) prove that the rule which follows is correct: > > If x = y then y = x. > > > 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 everything-list+unsubscr...@googlegroups.com. > To post to this group, send email to everything-list@googlegroups.com. > Visit this group at https://groups.google.com/group/everything-list. > For more options, visit https://groups.google.com/d/optout. -- 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 everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
Re: Combinator joker (a note in passing on formal combinator theory)
Well, you must assume the principle of identity at the beginning, otherwise all your other assumptions will be their own negations. -- 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 everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
Combinator joker (a note in passing on formal combinator theory)
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 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, Hint use 1) and 4). 2) prove that the rule which follows is correct: If x = y then y = x. 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 everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
