la tersmu

From Lojban
Jump to navigation Jump to search

la tersmu, a semantic parser for lojban written in Haskell.

The parser accepts almost arbitrary grammatical Lojban, and translates the input to a predicate logic form. It currently mostly ignores indicators and frees, even those which arguably should be rendered in the logic, but otherwise implements every construction bar a handful of obscure or difficult cases (detailed in the file BUGS in the source tree).

Its primary purpose, at least in its current incarnation, is to implement a comprehensive set of rules to handle the interactions between the various logical features of Lojban - such as the variously positioned connectives, embedded quantifiers and modal operators, sumti and bridi anaphora, and so on.

One can test it without installing, either by talking to the bot 'tersmus' on IRC (#lojban on irc.freenode.net), or by doing ssh request to thegonz.net with username 'tersmu', password 'tersmu'.

Baseline lojban implemented, CLL+xorlo, where possible.

Despite extensive attempts, the author could not find reasonable comprehensive rules which incorporate CLL's account of na as a selbri tag, nor CLL's rules on scope of variables outside of a prenex. Instead, bare na is treated as identical to naku, and (roughly) unprenexed variables as scoping only over the remainder of the sentence in which they appear. CLL's rules on rebinding bound variables and on "simultaneous quantification" in termsets are ignored, since neither fits with the idea that PA da should introduce a quantifier in the usual sense of predicate logic.

There are also many cases, too numerous to list here, where baseline documentation is not detailed enough to completely determine the transformation rules. go'i is a good example. In these cases, the BPFK pages have been the guide in the first instance, and then by parsimony, general logical and Lojbanic intuition, usage, and in some cases simply what fits best with the rest of the algorithm. The writings of xorxes, on the BPFK sections and elsewhere, clarified many points; discussions on IRC and the mailing list this list were valuable in clarifying others.

In many cases making any questionable decisions have been avoided at all by simply copying Lojbanic constructs into the logic. So, for example, the logic allows for non-logically connected propositions precisely analogous to Lojban's non-logically connected sentences. So what is called "logic" here doesn't even have an obvious semantics, so arguably isn't worthy of the term; there's plenty of room here for future work.

Source

  • Source code (GPLv3) [previous location 1, 2]
    • If you have cabal, the haskell package management system, tersmu can be installed with $ cabal update && cabal install tersmu.

Some examples

  • ro da poi verba cu prami lo mamta be da
    • FA x1:(verba(_)). mamta(f0(x1),x1)
    • FA x1:(verba(_)). prami(x1,f0(x1))
    • ro da poi ke'a verba ku'o zo'u li ma'o fyno mo'e da lo'o mamta da
    • .i ro da poi ke'a verba ku'o zo'u da prami li ma'o fyno mo'e da lo'o
      • Here, we interpret lo mamta be da as a function from children to their mothers; the first proposition expresses this, and the second is then the main statement.
  • examples from CLL:

Legend

  • FA is for all
  • EX is there exists
  • /\ is and
  • f0 is a function (glorked from context)