Return-path: Envelope-to: lojban-list-archive@lojban.org Delivery-date: Thu, 01 Apr 2021 10:02:56 -0700 Received: from mail-oi1-f187.google.com ([209.85.167.187]:48575) by stodi.digitalkingdom.org with esmtps (TLS1.3) tls TLS_AES_128_GCM_SHA256 (Exim 4.94) (envelope-from ) id 1lS0iY-00GSUu-9l for lojban-list-archive@lojban.org; Thu, 01 Apr 2021 10:02:56 -0700 Received: by mail-oi1-f187.google.com with SMTP id b1sf2375227oib.15 for ; Thu, 01 Apr 2021 10:02:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:reply-to:precedence:mailing-list :list-id:list-post:list-help:list-archive:list-subscribe :list-unsubscribe; bh=GNqjVQZ3kTrpsrmNfIyd7Gf+bl6URsPEa57yCTXyrPA=; b=mQ2lt2jQKcNQ/QfN8aIZ+VgkOfggOntyGaXfxEwtPKzF4jB0l7onI8zJ1pS4mhva7x 1GW/E7qQYbGHqQ+z6wCggKdQJadf+AwaB39CqfIxjWu//jObbP/h9f93RKuXWQ0PK1Vw dvrxXaUxx37y+IVUtl5Fj+lGMw9hRYl5VCqrgHSwEtbe9yxtve6DAnOWxjc2vJLX86ad e/Qifbtp2PnVVT2DKXsnzr117jlj8+XIMoPud9m251UvVQ/rqBRZ7/l64OpLfAO09jxG kDIA8upHapSrzpnCH5FHM6xWdgsr/pBNn0DH24oEGlkavKfeppjm7+bLBQFwAOWal/3E 55cQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:reply-to:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=GNqjVQZ3kTrpsrmNfIyd7Gf+bl6URsPEa57yCTXyrPA=; b=lvYNTe/qirfsPfc6d7rivD824anGpa88NKnkJytA03LqIsoxGkH8L+A9Y0bcjiMPhk xiq+WdFSyc8rQaixFvm9OE8ybUT21/lkZ0La2MSBUtgxfTXUY29Xhn32UL8BNkpivvRC cyVJp+pfv7a3R+23QPm9eimuyP/Z62gA+yiiNsejZUs0OAvoAlFoncViW0BCfwbO2Fyu ueErxeyINXkvmN77pM3yq9T35Nz/fkAJovufb8BIuiq52BVbBsaL93J3Bn3OyBOqt9Ip /Hy6Ag/o5DqvpFGdumM2sTmZ21Y7PTJzZXr+LUeP2edOPNS1dc/9WcGvdzuSOUj02hJX xQ7w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:reply-to :precedence:mailing-list:list-id:x-spam-checked-in-group:list-post :list-help:list-archive:list-subscribe:list-unsubscribe; bh=GNqjVQZ3kTrpsrmNfIyd7Gf+bl6URsPEa57yCTXyrPA=; b=cOz7v/ycxbmCk2o0QfXLpUQzvINEDwo+EG5//1LmkmZNdxQaEbjIu3i7i0c01+1Fse KcvEOyWSYah/+yCd/gB+Fzrl0BdfomlK1rHo9QHf3Sn4wc3Brl9zP8zCagJGt++oM/2U gNFOxtMNjkpiQB7xSjdawnHTd3AzYiurxbLFXEMOkfxzinCFOCUMBG5camhP82kWZO1c f371eIUJXCwHUUsmm7Nu1a5AZnLa7qQ8bW/gQW2vgzJNGwO6f4ZKdOriYrXfLBjH+038 HyoMap3seB3k2qke6NmrLougHf4jY3fQXzWzXkEmu9tm2EVYBQS83a+dLM9PJaoGLWnM +E2Q== Sender: lojban@googlegroups.com X-Gm-Message-State: AOAM533SNzgC28roFy2Y5FFkO/cXQUDlWtcN/WE72Pjpv0wOq8KMston tEN4ugQFwnDayarQnamqIfI= X-Google-Smtp-Source: ABdhPJxpFfS3ielGCyGdGX2PPp81o1oR/wR/9H8r0fambM0aSNr95/VsJsBnxKEUaZ1lAVZwYYH08g== X-Received: by 2002:a9d:6296:: with SMTP id x22mr7554409otk.196.1617296569239; Thu, 01 Apr 2021 10:02:49 -0700 (PDT) X-BeenThere: lojban@googlegroups.com Received: by 2002:aca:c650:: with SMTP id w77ls1433200oif.1.gmail; Thu, 01 Apr 2021 10:02:48 -0700 (PDT) X-Received: by 2002:a05:6808:1405:: with SMTP id w5mr6754353oiv.48.1617296568528; Thu, 01 Apr 2021 10:02:48 -0700 (PDT) Date: Thu, 1 Apr 2021 10:02:47 -0700 (PDT) From: "gleki.is...@gmail.com" To: lojban Message-Id: <2d3e019b-5f57-4288-98a8-cc7fe3bf41a2n@googlegroups.com> In-Reply-To: References: Subject: [lojban] Re: Lojban is a logical failure MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_8044_1916621651.1617296567990" X-Original-Sender: gleki.is.my.name@gmail.com Reply-To: lojban@googlegroups.com Precedence: list Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com List-ID: X-Spam-Checked-In-Group: lojban@googlegroups.com X-Google-Group-Id: 1004133512417 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , X-Spam-Score: -2.6 (--) X-Spam_score: -2.6 X-Spam_score_int: -25 X-Spam_bar: -- ------=_Part_8044_1916621651.1617296567990 Content-Type: multipart/alternative; boundary="----=_Part_8045_2106950700.1617296567990" ------=_Part_8045_2106950700.1617296567990 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Em quinta-feira, 1 de abril de 2021 =C3=A0s 18:08:28 UTC+3, mostawe...@gmai= l.com=20 escreveu: > Hey all, > > Time for the sort-of-annual reminder that Lojban falls far short of its= =20 > 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=20 > [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= =20 > sentence > * A collection of rewrite rules which each match sequences of words withi= n=20 > well-formed sentences and replace them with new sequences of words which= =20 > are still well-formed > > We have two of three, for what it's worth. The failure is in this third= =20 > component. If we had all three, then we might call Lojban a *type theory*= =20 > [1]. In a type theory, we start with a sentence, and then apply rewrite= =20 > rules to create new sentences. A sequence of rewrite rules, along with a= =20 > starting sentence, is called a *proof* when the rules can be applied in= =20 > sequence to the starting sentence in order to produce a new final sentenc= e. > > The defining feature of type theory is types. A type is a collection of= =20 > proofs, called *elements* of the type, which might be equivalent to each= =20 > other. To show equivalence for two objects, we would need a pair of proof= s=20 > which transform one object into another. We can also do this for two=20 > different proofs which lead to the same element in the same type, by=20 > transforming one proof into another, and so on. (This leads to [2].) > > Contrary to popular belief, types are emergent features of type theory;= =20 > they do not have to be predefined. If we had a collection of rewrite rule= s=20 > for Lojban, then we could discover types within Lojban's existing corpus.= A=20 > ready stream of examples comes from the fact that sets are like partial= =20 > (*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=20 > native type theory is one which is generated directly from the three=20 > components I mentioned earlier, but ignoring any "types" which might be= =20 > defined internally already. For example, {ctaipe} does not actually refer= =20 > to Lojban's types. The native type theory could be directly put to use=20 > 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=20 > world [8] > * To compile Lojban utterances into executable programs [9] > > Iterating on CLL has not produced the rewrite rules that we might desire.= =20 > It sketches several rules and even gives some examples for the "logical"= =20 > connectives, but it is far from complete. Similarly, la brismu suggests a= =20 > handful of rewrite rules borrowed from CLL and other logics, but is missi= ng=20 > 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 care= d=20 > to learn the relevant maths. > Do we have a plan? No deadlines but some plan might be needed. Where to=20 start from? Can we solve problems iteratively?=20 > > 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]=20 > https://golem.ph.utexas.edu/category/2021/03/native_type_theory_part_2.ht= ml > [5]=20 > 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/ > > --=20 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 e= mail to lojban+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= lojban/2d3e019b-5f57-4288-98a8-cc7fe3bf41a2n%40googlegroups.com. ------=_Part_8045_2106950700.1617296567990 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

E= m quinta-feira, 1 de abril de 2021 =C3=A0s 18:08:28 UTC+3, mostawe...@gmail= .com escreveu:
Hey all,

Time for the sort-of-annual reminder that Lojb= an falls far short of its goals. I'll spell out an explicit recipe for achi= eving those goals.

Suppose that Lojban were lo= gical; that is, suppose that it has a logic [0]. A logic has three componen= ts:

* A collection of letters which form a collect= ion of words
* A grammar which indicates whether a sequence of wo= rds is a well-formed sentence
* A collection of rewrite rules whi= ch each match sequences of words within well-formed sentences and replace t= hem with new sequences of words which are still well-formed

<= /div>
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 th= eory* [1]. In a type theory, we start with a sentence, and then apply rewri= te 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 se= quence to the starting sentence in order to produce a new final sentence.

The defining feature of type theory is types. A typ= e 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 nee= d 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 ty= pe, by transforming one proof into another, and so on. (This leads to [2].)=

Contrary to popular belief, types are emergent fe= atures of type theory; they do not have to be predefined. If we had a colle= ction of rewrite rules for Lojban, then we could discover types within Lojb= an's existing corpus. A ready stream of examples comes from the fact that s= ets are like partial (*truncated*) types; they have elements and equivalenc= e, but no proofs.

In fact, this would give the nat= ive type theory [3][4][5] of Lojban. A native type theory is one which is g= enerated directly from the three components I mentioned earlier, but ignori= ng any "types" which might be defined internally already. For example, {cta= ipe} does not actually refer to Lojban's types. The native type theory coul= d be directly put to use computationally:

* To pro= ve formal facts about Lojban utterances [6]
* To optimize Lojban = utterances, shortening or clarifying them [7]
* To synthesize Loj= ban 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 migh= t desire. It sketches several rules and even gives some examples for the "l= ogical" connectives, but it is far from complete. Similarly, la brismu sugg= ests 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 mo= re.

Lojban only cosplays as a logical language. We= could fix that, if we cared to learn the relevant maths.

Do we have a plan? No deadlines but some plan migh= t be needed. Where to start from? Can we solve problems iteratively? <= /div>
Peace,
~ C.

[1] https://ncatlab.org/nlab/show/type+theory
[3] htt= ps://golem.ph.utexas.edu/category/2021/02/native_type_theory.html
[9] <= a href=3D"http://docs.idris-lang.org/en/latest/" target=3D"_blank" rel=3D"n= ofollow" data-saferedirecturl=3D"https://www.google.com/url?hl=3Dpt&q= =3Dhttp://docs.idris-lang.org/en/latest/&source=3Dgmail&ust=3D16173= 82905685000&usg=3DAFQjCNE9FsflR_vOQTlUW6Ts5hqY3MPxSQ">http://docs.idris= -lang.org/en/latest/

--
You received this message because you are subscribed to the Google Groups &= quot;lojban" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to lojban+unsub= scribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/l= ojban/2d3e019b-5f57-4288-98a8-cc7fe3bf41a2n%40googlegroups.com.
------=_Part_8045_2106950700.1617296567990-- ------=_Part_8044_1916621651.1617296567990--