Skip to main content

Posts

Showing posts from November, 2012

Interactivity, week 3

Last week I discussed some newly-explored proof-theoretic relationships between reasoning about process calculi and substructural logics, and vaguely mentioned some other programming models that I wanted to compare. Since then, I think I've come up with a way to phrase my research objective with this project: to relate the programming and reasoning methodologies surrounding interactivity through a common medium of proof theory.

That's not a thesis statement, but I figure it's better than "*waves hands excitedly* interactivity! Processes! Linear logic! Focusing!"

Anyway. What I've done so far has given me more questions than answers, but I like the questions a lot. The first of these questions I want to discuss in this post is "How can proof theory capture an appropriate notion of broadcast message replication?" To explain what I mean by that, I'll describe an example which I think captures some common interactive communication patterns.

Lights O…

Interactivity, week 2

My post about week 1 established a new research project I'm working on involving programming interactivity with substructural logic. This past week, I've been working on digesting some background and related work. One thing I did was spend a good long stretch working through the core ideas in Yuxin, Iliano, and Rob's paper Relating Reasoning Methods in Linear Logic and Process Algebra.

Linear contexts as processes
The point of the paper is to establish that a so-called "logical preorder" on contexts \[
\Delta \preceq_l \Delta'
\] defined (I'm simplifying to the strictly linear case1) as

\[
{For}\ {all}\ C, \Delta \vdash C \ {implies}\  \Delta' \vdash C
\]

where \[
\vdash
\] is entailment in linear logic, corresponds to traditional notions of contextual preorder in CCS/process algebras, which are defined coinductively by a reduction relation extended over a laundry list of structure-preserving properties. The symmetric closure of the contextual preorde…