Hacker News new | past | comments | ask | show | jobs | submit login
Programming Interactive Worlds with Linear Logic (cmu.edu)
188 points by ingve on Nov 28, 2015 | hide | past | web | favorite | 14 comments

I've spent probably 500-1000 hours thinking about linear logic and narrative structures and this blows everything I've put together out of the water... I'm very impressed, and am looking forward to reading it through.

If the author is reading this, please consider submitting your work to some literary theory journals. Literary theory has decayed into something tired and vague, and this sort of heroic formalism could really make a splash! I mean, this is actual literary theory!

The use of logic as a representation language for representing interactive games was pioneered by Richard Evans (AI lead on The Sims 3) over the years, and used in various of his games. The latest installment is [1], and the logic used is a peculiar modal logic whose key innovation is a lack of negation. Crazy!

I wonder what the relationship is between linear logic and the logic of [2].

[1] http://versu.com

[2] http://arxiv.org/abs/1411.7158

Where'd you hear that implementation detail about Versu? Due to all the legal wrangling around it, it's hard to find certain specifics...

edit: the magic of a little bird: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6...

I really enjoy non-classical logic, and all kinds of interesting systems arise when you remove one of the structural rules of classical or intuitionalistic logic. I'm at best an armchair logician, and I'd love for anyone to point out any flaws in my understanding, but I'll take a stab at describing linear logic and Evans' cathoristic logic.

Linear logic is obtained from a classical logic in which entailment is not monotonic or idempotent. That is, a statement X && Y && Y proves Z cannot be contracted to X && Y proves Z, nor can the statement X proves Z be weakened to X && Y proves Z. One interpretation of this lets you treat terms as resources which cannot be created out of thin air. This is really useful for modeling logical constraints on resources and their allocation.

Modal logics on the other hand are a very wide family of logic systems (see [0] for a diagram of some of the most simple modal logics) which introduce new operators to encode modality, a kind of qualification of the truth of a statement. For example a modal operator might encode that a statement is prohibited, that its truth is unknown, or that a statement will be true at some point in the future. These modal operators make modal logics useful for describing temporal constraints, or encoding logical statements about the belief of agents in a system (imagine giving each agent a modal operator B_i(X) which means, agent i believes X). In the latter case, different agents can hold incompatible beliefs without creating contradiction.

As I understand it, Evans' cathoristic logic (the name of which the paper claims has greek origins, meaning "to impose narrow boundaries") arises from the desire to simply express inferences between atomic sentences with the expressivity of natural language. First-order logic is able to encode many natural language statements, such as adverbials, inference from dyadic to monadic propositions, and handling incompatible statements. However, first-order logic requires us to introduce quantifiers to do so, vastly increasing the search space for decision and resolution of these propositions.

To get around the problem of quantifiers without losing expressivity, cathoristic logic uses subset of Hennessey-Milner logic[1] as a starting point. Negation is excluded, as it is the weakest form of encoding incompatibilities. For instance, in first-order logic, asserting "Pierre is the only king of Spain" is the same as saying "For all individuals other than Pierre, that individual is not the king of Spain". This weakness requires the knowledge-representer to include an axiom for every excluded possibility, or generalize the statement with a quantifier so that it no longer becomes atomic. Evans' therefore introduces the Tantum operator (written !A, for some set A) to express that the members of A exhaust all possibilities (almost like the latin abbreviation viz). Using the Tantum operator, we can reformulate the example above to be: "The king of spain is (Pierre && !{Pierre})".

Using this operator lets one make specific optimizations when running the decision algorithm, and the paper shows that it's able to perform decisions in quadratic time. If negation were included, the running time for decision would be superpolynomial.

Thanks for sharing the paper and prompting my read-through of it!

[0]: http://plato.stanford.edu/entries/logic-modal/#MapRelBetModL...

[1]: https://en.wikipedia.org/wiki/Hennessy%E2%80%93Milner_logic

For those unfamiliar I'll just share an short pithy example of simple vs linear logic I first heard from my brother:


  if $5 then pizza
  if $5 then beer
  therefor: pizza AND beer

  if $5 then pizza
  if $5 then beer
  therefor: pizza OR beer
There are other aspects, but this key difference lets linear logic model resource consumption.

Interesting, how about:

    if $5 then pizza
    if $2 then beer
The priority might be to acquire the most valuable item (pizza), or to spend the most money (3 beers), or to have the most money left over with nothing left to buy (pizza again), etc. Is there a way to describe those kinds of goals/constraints within the same system?

Linear logic itself doesn't express goals or constraints, just what can be accomplished with a given set of resources.

In the example you gave:

    if $5 then pizza
    if $2 then beer
    therefore, (pizza and $1) OR (beer and $4) OR (beer and beer and $2) OR (beer and beer and beer) OR $6

Here's the Ceptre repo. The interpreter is written in Standard ML.


This looks a lot like STRIPS planning http://www.primaryobjects.com/2015/11/06/artificial-intellig...

The Ceptre tutorial even has the classic example of moving blocks on a table. It's a different language than STRIPS (using PDDL), but seems a similar idea.

Apparently this is where you can play the games created by their generative algorithm: http://play.typesafety.net/

Hooray, finally somebody uses relevant logic without contraction and without the distribution of conjunction over disjunction!

"Ceptre: A Language for Modeling Generative Interactive Systems" by Chris Martens Strange Loop


Brain broken. (applause)


> What is the meaning of this work?, I couldn't get that in my very quick glance at this work.

you are aware that this document, being a phd thesis, is the result of years of original research and writing, right?

Registration is open for Startup School 2019. Classes start July 22nd.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact