Envelope-to: lojban-list-archive@lojban.org
Delivery-date: Thu, 01 Apr 2021 10:07:31 -0700
Sender: lojban@googlegroups.com
Date: Thu, 1 Apr 2021 10:07:21 -0700 (PDT)
From: Corbin Simpson <mostawesomedude@gmail.com>
To: lojban <lojban@googlegroups.com>
Message-Id: <67b9585f-d8f5-4309-ac18-148512de6c72n@googlegroups.com>
In-Reply-To: <555219299.1422165.1617294275560@mail.yahoo.com>
References: <ac15b0d5-c27c-4d8c-a459-4f80e9970bddn@googlegroups.com>
 <555219299.1422165.1617294275560@mail.yahoo.com>
Subject: Re: [lojban] Lojban is a logical failure
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_11452_88402828.1617296841927"
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
X-Spam_score: -2.6
X-Spam_score_int: -25
X-Spam_bar: --

------=_Part_11452_88402828.1617296841927
Content-Type: multipart/alternative; 
	boundary="----=_Part_11453_614132737.1617296841927"

------=_Part_11453_614132737.1617296841927
Content-Type: text/plain; charset="UTF-8"

Sure. So, instead of waiting for rewrite rules to be issued like manna from 
heaven, we could explicitly write out rules which implement the behaviors 
that we typically imply in casual usage. IOW where are all the fluent 
speakers; they should already know these rules by heart and could just 
write them down for us~

CLL gives suggested equivalences for {se} (CLL 5.11), {ka} (CLL 11.4), 
distributive laws (CLL 14.8), forethought and afterthought connectors (CLL 
14.5), etc. See la brismu [0] for a detailed exploration. lojban.io [1] 
uses these rules to partially canonicalize bridi.

[0] 
https://github.com/MostAwesomeDude/brismu/blob/master/0-midju/2-proofs.md
[1] https://lojban.io/

On Thursday, April 1, 2021 at 9:24:38 AM UTC-7 clifford wrote:

> n lacks the underlying HOIL and derivation rules for it and so can never 
> achieve even its goAL OF MONOPrsing, but eventually that comes to the same.
>
>
> On Thursday, April 1, 2021, 10:37:57 AM CDT, Corbin Simpson <
> mostawe...@gmail.com> wrote: 
>
>
> Hey all,
>
> Time for the sort-of-annual reminder that Lojban falls far short of its 
> goals. I'll spell out an explicit recipe for achieving those goals.
>
> Suppose that Lojban were logical; that is, suppose that it has a logic 
> [0]. A logic has three components:
>
> * A collection of letters which form a collection of words
> * A grammar which indicates whether a sequence of words is a well-formed 
> sentence
> * A collection of rewrite rules which each match sequences of words within 
> well-formed sentences and replace them with new sequences of words which 
> are still well-formed
>
> We have two of three, for what it's worth. The failure is in this third 
> component. If we had all three, then we might call Lojban a *type theory* 
> [1]. In a type theory, we start with a sentence, and then apply rewrite 
> rules to create new sentences. A sequence of rewrite rules, along with a 
> starting sentence, is called a *proof* when the rules can be applied in 
> sequence to the starting sentence in order to produce a new final sentence.
>
> The defining feature of type theory is types. A type is a collection of 
> proofs, called *elements* of the type, which might be equivalent to each 
> other. To show equivalence for two objects, we would need a pair of proofs 
> which transform one object into another. We can also do this for two 
> different proofs which lead to the same element in the same type, by 
> transforming one proof into another, and so on. (This leads to [2].)
>
> Contrary to popular belief, types are emergent features of type theory; 
> they do not have to be predefined. If we had a collection of rewrite rules 
> for Lojban, then we could discover types within Lojban's existing corpus. A 
> ready stream of examples comes from the fact that sets are like partial 
> (*truncated*) types; they have elements and equivalence, but no proofs.
>
> In fact, this would give the native type theory [3][4][5] of Lojban. A 
> native type theory is one which is generated directly from the three 
> components I mentioned earlier, but ignoring any "types" which might be 
> defined internally already. For example, {ctaipe} does not actually refer 
> to Lojban's types. The native type theory could be directly put to use 
> computationally:
>
> * To prove formal facts about Lojban utterances [6]
> * To optimize Lojban utterances, shortening or clarifying them [7]
> * To synthesize Lojban utterances which describe a partially-specified 
> world [8]
> * To compile Lojban utterances into executable programs [9]
>
> Iterating on CLL has not produced the rewrite rules that we might desire. 
> It sketches several rules and even gives some examples for the "logical" 
> connectives, but it is far from complete. Similarly, la brismu suggests a 
> handful of rewrite rules borrowed from CLL and other logics, but is missing 
> the tense system, BAI, Lojban-in-Lojban grammar, mekso, and much more.
>
> Lojban only cosplays as a logical language. We could fix that, if we cared 
> to learn the relevant maths.
>
> Peace,
> ~ C.
>
> [0] https://ncatlab.org/nlab/show/logic
> [1] https://ncatlab.org/nlab/show/type+theory
> [2] https://ncatlab.org/nlab/show/homotopy%20type%20theory
> [3] https://golem.ph.utexas.edu/category/2021/02/native_type_theory.html
> [4] 
> https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_2.html
> [5] 
> https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_3_1.html
> [6] http://us.metamath.org/
> [7] https://egraphs-good.github.io/
> [8] https://github.com/webyrd/Barliman
> [9] http://docs.idris-lang.org/en/latest/
>
> -- 
> You received this message because you are subscribed to the Google Groups 
> "lojban" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to lojban+un...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/lojban/ac15b0d5-c27c-4d8c-a459-4f80e9970bddn%40googlegroups.com 
> <https://groups.google.com/d/msgid/lojban/ac15b0d5-c27c-4d8c-a459-4f80e9970bddn%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>

-- 
You received this message because you are subscribed to the Google Groups "lojban" group.
To unsubscribe from this group and stop receiving emails from it, send an email to lojban+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/lojban/67b9585f-d8f5-4309-ac18-148512de6c72n%40googlegroups.com.

------=_Part_11453_614132737.1617296841927
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div>Sure. So, instead of waiting for rewrite rules to be issued like manna=
 from heaven, we could explicitly write out rules which implement the behav=
iors that we typically imply in casual usage. IOW where are all the fluent =
speakers; they should already know these rules by heart and could just writ=
e them down for us~</div><div><br></div><div>CLL gives suggested equivalenc=
es for {se} (CLL 5.11), {ka} (CLL 11.4), distributive laws (CLL 14.8), fore=
thought and afterthought connectors (CLL 14.5), etc. See la brismu [0] for =
a detailed exploration. lojban.io [1] uses these rules to partially canonic=
alize bridi.<br></div><div><br></div><div>[0] https://github.com/MostAwesom=
eDude/brismu/blob/master/0-midju/2-proofs.md</div><div>[1] https://lojban.i=
o/<br></div><br><div class=3D"gmail_quote"><div dir=3D"auto" class=3D"gmail=
_attr">On Thursday, April 1, 2021 at 9:24:38 AM UTC-7 clifford wrote:<br/><=
/div><blockquote class=3D"gmail_quote" style=3D"margin: 0 0 0 0.8ex; border=
-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;"><div><div style=3D=
"font-family:Helvetica Neue,Helvetica,Arial,sans-serif;font-size:13px"><div=
></div>
        <div dir=3D"ltr">n lacks the underlying HOIL and derivation rules f=
or it and so can never achieve even its goAL OF MONOPrsing, but eventually =
that comes to the same.</div><div dir=3D"ltr"><br></div><div><br></div>
       =20
        </div><div>
            <div style=3D"font-family:&#39;Helvetica Neue&#39;,Helvetica,Ar=
ial,sans-serif;font-size:13px;color:#26282a"></div></div></div><div><div><d=
iv style=3D"font-family:&#39;Helvetica Neue&#39;,Helvetica,Arial,sans-serif=
;font-size:13px;color:#26282a">
               =20
                <div>
                    On Thursday, April 1, 2021, 10:37:57 AM CDT, Corbin Sim=
pson &lt;<a href data-email-masked rel=3D"nofollow">mostawe...@gmail.com</a=
>&gt; wrote:
                </div>
                <div><br></div>
                <div><br></div>
                </div></div></div><div><div><div style=3D"font-family:&#39;=
Helvetica Neue&#39;,Helvetica,Arial,sans-serif;font-size:13px;color:#26282a=
"><div><div>Hey all,<div><br></div><div>Time for the sort-of-annual reminde=
r that Lojban falls far short of its goals. I&#39;ll spell out an explicit =
recipe for achieving those goals.<br></div><div><br></div><div>Suppose that=
 Lojban were logical; that is, suppose that it has a logic [0]. A logic has=
 three components:</div><div><br></div><div>* A collection of letters which=
 form a collection of words</div><div>* A grammar which indicates whether a=
 sequence of words is a well-formed sentence</div><div>* A collection of re=
write rules which each match sequences of words within well-formed sentence=
s and replace them with new sequences of words which are still well-formed<=
/div><div><br></div><div>We have two of three, for what it&#39;s worth. The=
 failure is in this third component. If we had all three, then we might cal=
l Lojban a *type theory* [1]. In a type theory, we start with a sentence, a=
nd then apply rewrite rules to create new sentences. A sequence of rewrite =
rules, along with a starting sentence, is called a *proof* when the rules c=
an be applied in sequence to the starting sentence in order to produce a ne=
w final sentence.</div><div><br></div><div>The defining feature of type the=
ory is types. A type is a collection of proofs, called *elements* of the ty=
pe, which might be equivalent to each other. To show equivalence for two ob=
jects, we would need a pair of proofs which transform one object into anoth=
er. We can also do this for two different proofs which lead to the same ele=
ment in the same type, by transforming one proof into another, and so on. (=
This leads to [2].)</div><div><br></div><div>Contrary to popular belief, ty=
pes are emergent features of type theory; they do not have to be predefined=
. If we had a collection of rewrite rules for Lojban, then we could discove=
r types within Lojban&#39;s existing corpus. A ready stream of examples com=
es from the fact that sets are like partial (*truncated*) types; they have =
elements and equivalence, but no proofs.</div><div><br></div><div>In fact, =
this would give the native type theory [3][4][5] of Lojban. A native type t=
heory is one which is generated directly from the three components I mentio=
ned earlier, but ignoring any &quot;types&quot; which might be defined inte=
rnally already. For example, {ctaipe} does not actually refer to Lojban&#39=
;s types. The native type theory could be directly put to use computational=
ly:</div><div><br></div><div>* To prove formal facts about Lojban utterance=
s [6]</div><div>* To optimize Lojban utterances, shortening or clarifying t=
hem [7]</div><div>* To synthesize Lojban utterances which describe a partia=
lly-specified world [8]<br></div><div>* To compile Lojban utterances into e=
xecutable programs [9]</div><div><br></div><div>Iterating on CLL has not pr=
oduced the rewrite rules that we might desire. It sketches several rules an=
d even gives some examples for the &quot;logical&quot; connectives, but it =
is far from complete. Similarly, la brismu suggests a handful of rewrite ru=
les borrowed from CLL and other logics, but is missing the tense system, BA=
I, Lojban-in-Lojban grammar, mekso, and much more.</div><div><br></div><div=
>Lojban only cosplays as a logical language. We could fix that, if we cared=
 to learn the relevant maths.<br></div><div><br></div><div>Peace,<br></div>=
<div>~ C.<br></div><div><br></div><div>[0] <a href=3D"https://ncatlab.org/n=
lab/show/logic" target=3D"_blank" rel=3D"nofollow" data-saferedirecturl=3D"=
https://www.google.com/url?hl=3Den&amp;q=3Dhttps://ncatlab.org/nlab/show/lo=
gic&amp;source=3Dgmail&amp;ust=3D1617382883515000&amp;usg=3DAFQjCNE41GO2VLR=
J9KeGd6pMIp-aE0AOmQ">https://ncatlab.org/nlab/show/logic</a><br></div><div>=
[1] <a href=3D"https://ncatlab.org/nlab/show/type+theory" target=3D"_blank"=
 rel=3D"nofollow" data-saferedirecturl=3D"https://www.google.com/url?hl=3De=
n&amp;q=3Dhttps://ncatlab.org/nlab/show/type%2Btheory&amp;source=3Dgmail&am=
p;ust=3D1617382883515000&amp;usg=3DAFQjCNGGm6hFHImF6M2hftxbdt2wnCHl9w">http=
s://ncatlab.org/nlab/show/type+theory</a></div><div>[2] <a href=3D"https://=
ncatlab.org/nlab/show/homotopy%20type%20theory" target=3D"_blank" rel=3D"no=
follow" data-saferedirecturl=3D"https://www.google.com/url?hl=3Den&amp;q=3D=
https://ncatlab.org/nlab/show/homotopy%2520type%2520theory&amp;source=3Dgma=
il&amp;ust=3D1617382883515000&amp;usg=3DAFQjCNFpxn2f8QqGE7GYZM69c8upArJ_zA"=
>https://ncatlab.org/nlab/show/homotopy%20type%20theory</a></div><div>[3] <=
a href=3D"https://golem.ph.utexas.edu/category/2021/02/native_type_theory.h=
tml" target=3D"_blank" rel=3D"nofollow" data-saferedirecturl=3D"https://www=
.google.com/url?hl=3Den&amp;q=3Dhttps://golem.ph.utexas.edu/category/2021/0=
2/native_type_theory.html&amp;source=3Dgmail&amp;ust=3D1617382883515000&amp=
;usg=3DAFQjCNGgIzl8v-F9Ql2oRaMMV5Ui84kpwA">https://golem.ph.utexas.edu/cate=
gory/2021/02/native_type_theory.html</a><br></div><div>[4] <a href=3D"https=
://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_2.html" tar=
get=3D"_blank" rel=3D"nofollow" data-saferedirecturl=3D"https://www.google.=
com/url?hl=3Den&amp;q=3Dhttps://golem.ph.utexas.edu/category/2021/03/native=
_type_theory_part_2.html&amp;source=3Dgmail&amp;ust=3D1617382883515000&amp;=
usg=3DAFQjCNFFK-5TS3gjGrMsq1b4x-8_F8fXBw">https://golem.ph.utexas.edu/categ=
ory/2021/03/native_type_theory_part_2.html</a><br></div><div>[5] <a href=3D=
"https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_3_1.h=
tml" target=3D"_blank" rel=3D"nofollow" data-saferedirecturl=3D"https://www=
.google.com/url?hl=3Den&amp;q=3Dhttps://golem.ph.utexas.edu/category/2021/0=
3/native_type_theory_part_3_1.html&amp;source=3Dgmail&amp;ust=3D16173828835=
15000&amp;usg=3DAFQjCNF1Q2rc0znKjMwQaclrAijvH1AehA">https://golem.ph.utexas=
.edu/category/2021/03/native_type_theory_part_3_1.html</a></div><div>[6] <a=
 href=3D"http://us.metamath.org/" target=3D"_blank" rel=3D"nofollow" data-s=
aferedirecturl=3D"https://www.google.com/url?hl=3Den&amp;q=3Dhttp://us.meta=
math.org/&amp;source=3Dgmail&amp;ust=3D1617382883515000&amp;usg=3DAFQjCNHx7=
gBN6R1gzAVGKlT2sZtaEUuSGg">http://us.metamath.org/</a></div><div>[7] <a hre=
f=3D"https://egraphs-good.github.io/" target=3D"_blank" rel=3D"nofollow" da=
ta-saferedirecturl=3D"https://www.google.com/url?hl=3Den&amp;q=3Dhttps://eg=
raphs-good.github.io/&amp;source=3Dgmail&amp;ust=3D1617382883515000&amp;usg=
=3DAFQjCNEws6ryHxG7UGldcmmZ3xE_hkxnbA">https://egraphs-good.github.io/</a><=
/div><div>[8] <a href=3D"https://github.com/webyrd/Barliman" target=3D"_bla=
nk" rel=3D"nofollow" data-saferedirecturl=3D"https://www.google.com/url?hl=
=3Den&amp;q=3Dhttps://github.com/webyrd/Barliman&amp;source=3Dgmail&amp;ust=
=3D1617382883515000&amp;usg=3DAFQjCNGuyY8eT-K88G3HblHxxLGcmwAVUw">https://g=
ithub.com/webyrd/Barliman</a></div><div>[9] <a href=3D"http://docs.idris-la=
ng.org/en/latest/" target=3D"_blank" rel=3D"nofollow" data-saferedirecturl=
=3D"https://www.google.com/url?hl=3Den&amp;q=3Dhttp://docs.idris-lang.org/e=
n/latest/&amp;source=3Dgmail&amp;ust=3D1617382883515000&amp;usg=3DAFQjCNEm_=
Xut-W-cMTfUWMTkEZgnpepVzQ">http://docs.idris-lang.org/en/latest/</a><br></d=
iv><div><br></div>

<p></p></div></div></div></div></div><div><div><div style=3D"font-family:&#=
39;Helvetica Neue&#39;,Helvetica,Arial,sans-serif;font-size:13px;color:#262=
82a"><div><div>

-- <br>
You received this message because you are subscribed to the Google Groups &=
quot;lojban&quot; group.<br>
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a rel=3D"nofollow noopener noreferrer" href data-email-masked>lojb=
an+un...@googlegroups.com</a>.<br>
To view this discussion on the web visit <a rel=3D"nofollow noopener norefe=
rrer" href=3D"https://groups.google.com/d/msgid/lojban/ac15b0d5-c27c-4d8c-a=
459-4f80e9970bddn%40googlegroups.com?utm_medium=3Demail&amp;utm_source=3Dfo=
oter" target=3D"_blank" data-saferedirecturl=3D"https://www.google.com/url?=
hl=3Den&amp;q=3Dhttps://groups.google.com/d/msgid/lojban/ac15b0d5-c27c-4d8c=
-a459-4f80e9970bddn%2540googlegroups.com?utm_medium%3Demail%26utm_source%3D=
footer&amp;source=3Dgmail&amp;ust=3D1617382883515000&amp;usg=3DAFQjCNEV06Fs=
nMqHuva1TDA8WIr_ExHVKg">https://groups.google.com/d/msgid/lojban/ac15b0d5-c=
27c-4d8c-a459-4f80e9970bddn%40googlegroups.com</a>.<br>
</div></div>
            </div>
        </div></div></blockquote></div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;lojban&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:lojban+unsubscribe@googlegroups.com">lojban+unsub=
scribe@googlegroups.com</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/d/msgid/lojban/67b9585f-d8f5-4309-ac18-148512de6c72n%40googlegroups.com?=
utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.com/d/msgid/l=
ojban/67b9585f-d8f5-4309-ac18-148512de6c72n%40googlegroups.com</a>.<br />

------=_Part_11453_614132737.1617296841927--

------=_Part_11452_88402828.1617296841927--