As promised, today, I’m going to show the Kripke semantics model for intuitionistic logic.
The Kripke Model for Intuitionistic Logic
7 Replies
Category Archives: Good Math
Kripke Semantics and Models for Intuitionistic Logic
To be able to really talk about what a logic (or a calculus) means, you need to define a model of that logic. A model is a way of associating entities in the logic/calculus with some kind of real entity in a way where all statements in the logic about the logical entity will also be true about the real-world entity. Models are incredibly important, because it’s relatively easy to design a logic which looks as if it’s perfectly valid, but which contains some subtle error which leads to it being essentially meaningless – showing a model for a logic guarantees that that can’t happen.
Intuitionistic Logic (partial rerun)
I’m incredibly busy right now adjusting to my new job and my new commute, which is leaving me less time than usual for blogging. So I’m going to raid the archives, and bring back some interesting things that appeared on the old Blogger blog, but were never posted here. As usual, that will involve some cleanups and rewrites, so this won’t be identical to the original posts.
I’ve written about logic before, and mentioned intuitionistic logic at least in passing. Intuitionistic logic is an interesting subject. Intuitionistic logic is a variation of predicate logic which is built on the idea that there should be a stronger notion of “truth” in logic: that the strict categorization of all statements in classical logic as either true or false is too strong. In intuitionistic logic, a statement is only true if you can prove that it is true. It is not enough to prove that it’s opposite is false: In propositional logic, it is not the case that ¬¬P→P.
More π-Calculus Games
Ok. So I’m still tweaking syntax, to try to find a way of writing π-calculus in a way that’s
easy for me to write in my editor, and for you to read in your browser. Here’s the latest version:
- Sequential Composition:
Process1.Process2. - Send expressions:
!channel(tuple).Process - Receive expressions:
?channel(tuple).Process - New channel expression
new(name,...) { Process } - Process duplication expression:
*(Process) - Parallel composition:
Process1 | Process2. - Choice composition:
Process1 + Process2. - Null process:
∅
So, in this syntax, the final version of the storage cell from yesterdays post
is:
NewCell[creator,initval]=new(read,write){ (Cell[read,write,initval]
| !creator(read,write)) }
Cell[read,write,val]=( !read(val).Cell[read,write,val]
+ ?write(v).Cell[read,write,v])
Now, let’s try to use π-calculus to do something that actually involves real concurrency.
Programming with Shapes: Clunk
Today’s bit of pathology is a really silly, and really fun language called Clunk, with a downloadable package containing a perl implementation here. I’m
not sure that it’s Turing compete, but my best guess is that it is. It’s another two dimensional
language, but it’s very different from any of the other 2d languages that we’ve look at, because it
doesn’t rely on an instruction pointer moving around the playfield; instead, it computes by
creating an image by fitting together pieces according to some pre-determined rules.
Building Things in π-Calculus: Storage Cells
As a refresher for me, and to give some examples to help you guys understand it, I’m going to go through a couple of examples of interesting things you can build with π-calculus. We’ll start with a simple way of building mutable storage.
Basics: Parallel, Concurrent, and Distributed
This came up in a question in the post where I started to talk about π-calculus, but I thought it was an interesting enough topic to promote it up to a top-level post. If you listen to anyone talking about computers or software, there are three worlds you’ll constantly hear: parallel, concurrent, and distributed. At first glance, it sounds like they mean the same thing, but in fact, they’re three different things, and the differences are important.
An Experiment with π-calculus and Programming Language Design
I feel like a bit of a change of pace, and trying a bit of an experiment.
Re-reading Backus’s old FP work reminds me of what I was doing the last time I read it, which
was back in grad school. At the time, I was working on some stuff involving parallel computation,
and I discovered Robin Milner’s π-calculus as a tool for describing parallel computation. You
can think of π-calculus as being a sort of parallel (pun intended) for the λ-calculus: in
sequential, single-threaded computation, λ-calculus can be a great tool for describing what
things mean. But λ-calculus has absolutely no way of describing the concept of multiple
things happening at once. π-calculus is fundamentally built on the concept of multiple threads
which can only share information by passing messages.
There’s a reason that reading Backus made me think of this, beyond just the temporal coincendence of the fact that I was working with π-calculus the last time I read Backus’s
FP paper. One of the major points that Backus made was how poorly the vonNeumann model was
at describing many computations; that has become far more true in recent years. Even my laptop now has multiple processors; computation just isn’t single-threaded anymore. But most programming languages are basically deeply single-threaded. Even Haskell, for all of its functional
purity, isn’t particularly good at multi-threaded execution. But I’ve always thought it would be
a great idea to build a language around π-calculus the way that ML is built around λ-calculus.
So my experiment, such as it is, is to see if I can work through how to create an actual, useful, non-pathological programming language based on the π-calculus; and not just do that,
but do it publicly, here on the blog.
Backus's Idea of Functional Programming
In my earlier post about John Backus, I promised to write something about his later work on
functional programming languages. While I was in a doctors office getting treated for an awful
cough, I re-read his 1977 Turing Award Lecture. Even 30 years later, it remains a fascinating read,
and far from being dated, it’s positively astonishingly to see both how far-sighted Backus was, and how little progress we’ve actually made.
The Mapping of the E8 Lie Group (Minor Update)
I’ve been getting tons of mail from people in response to the announcement of the mapping of
the E8 Lie group, asking what a Lie group is, what E8 is, and why the mapping of E8 is such a big deal?