Linear logic

IRIS Wiki - Computational Models - Linear logic

Background

Linear logic was introduced by J.Y. Girard (1987) as a refinement of classical and intuitionistic logic. Instead of emphasizing truth, as in classical logic, or proof, as in intuitionistic logic, linear logic emphasizes the role of formulas as resources. Formulas are treated as resources which are produced and consumed. Every formula should be used exactly once in the derivation.

Description

Classical logic is commonly used for reasoning on eternal truth. Contrary to classical logic, linear logic is not used to determine whether an assertion is true or not but rather determines the validity of how the proof is achieved and the sequence of choices done.

The classical conjunction and its identity, ∧ and ⊤, split into the additive & (with) and ⊤ (top) and the multiplicative ⊗ (tensor) and 1 (one). Similarly, the classical disjunction and its identity, ∨ and ⊥, split into the additive ⊕ (oplus) and 0 (zero) and the multiplicative ⅋ (par) and ⊥ (bottom).

The used connectors for IS are:

• ⊸: Implication (imply), express the possibility of deduction
• ⊗ : Multiplicative conjunction (times), a set of resources (not ordered)
• !: Exponential conjunction (of course)
• ⊕: Additive disjunction (plus), internal choice
• ⊢: Turnstile, separate the left part (antecedent) and the right part (consequent) of a sequent.

Application to Interactive Storytelling

Greimas developed the narrative programme, as an abstract formula to represent an action. An action is defined as a succession from one state to another state where the subject gains or looses an object (conjunctive or disjunctive narrative programme). Finally, Greimas proposes an analysis of a story as a sequence of actions and linear logic was used as a computational model to compute the story and to perform analysis on the possible stories.

Examples

Mme Bovary analysis Madame Bovary - LL model

The L3i team developed a methodology to derive a computational model, starting from the Greimas Narrative Programme point of view (Cavazza et al., 2009).

An actor corresponds to an atom of LL. Disjunction and conjunction (following the Greimas analysis) corresponds to implication rules. A story is modeled by a sequent calculus. For example, segment of model of Mme Bovary:

• Junction. Listening discourse in the council room: talkingInTheCouncilRoom ⊗ RodolpheWantsToSeduceEmma ⊗ EmmaIsHappy ⊗ EmmaHasBeenSeducedByRodolphe ⊸ RodolpheInLoveWithEmma ⊗ EmmaIsHappy ⊗ EmmaHasBeenSeducedByRodolphe.
• History: ConversationWhileEmmaAndRodolpheGoToTheAgriculturalShow ⊗ TalkingInTheCouncilRoom ⊗ WeeksLater ⊗ ConversationAtBovaryHome ⊗ HorsebackRiding ⊗ ConverstationAtRodopheHome ⊗ RodolpheWantsToSeduceEmma ⊗ EmmaIsHappy ⊗ EmmaHasBeenSeducedByRodolphe ⊗ GoingToTheAgriculturalShow ⊗ ListeningDiscourseInTheCouncilRoom ⊗ LetSpendSomeTimesBeforeTheyMeetAgain ⊗ RodolpheVisitsEmma ⊗ HorsebackRiding ⊗ EmmaVisitsRodolphe ⊢ RodolpheAffectionsForEmmaBeginToWane ⊗ EmmaIsInLoveWithRodolphe ⊗ EmmaIsInLove

The LL model is based on the MALL (multiplicative additive linear logic) fragment of LL. MALL provability is PSPACE-complete.

References

• Cavazza, M., Champagnat, R., Leonardi, R. & the IRIS Consortium (2009). "The IRIS Network of Excellence: Future Directions in Interactive Storytelling". ICIDS 2009, Springer Verlag (To appear).
• Girard, J.-Y. (1987). Linear Logic, Theoretical Computer Science, London Mathematical 50:1, pp. 1-102.
• Lafont, Y. (1993). Introduction to Linear Logic. Lecture notes from TEMPUS Summer School on Algebraic and Categorical Methods in Computer Science, Brno, Czech Republic.
• Malpas, J. (2003). "Donald Davidson", The Stanford Encyclopedia of Philosophy (Winter 2003 Edition), Edward N. Zalta (ed.), http://plato.stanford.edu/archives/win2003/entries/davidson.