Kripke Semantics and Models for Intuitionistic Logic

Leave a reply

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.

Continue reading →

Intuitionistic Logic (partial rerun)

Leave a reply

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.

Continue reading →

More π-Calculus Games

Leave a reply

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:

  1. Sequential Composition: Process1.Process2.
  2. Send expressions: !channel(tuple).Process
  3. Receive expressions: ?channel(tuple).Process
  4. New channel expression new(name,...) { Process }
  5. Process duplication expression: *(Process)
  6. Parallel composition: Process1 | Process2.
  7. Choice composition: Process1 + Process2.
  8. 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.

Continue reading →

Programming with Shapes: Clunk

Leave a reply

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.

Continue reading →

Casey Luskin Demonstrates Cluelessness. Surprised?

Leave a reply

As usual, Casey Luskin over at DI’s media complaints division is playing games, misrepresenting people’s words in order to claim that that they’re misrepresenting IDists words. Nothing like the pot calling the kettle black, eh? This time, he’s accusing Ken Miller of misrepresenting Dembski
in a BBC documentary.

Continue reading →

Building Things in π-Calculus: Storage Cells

Leave a reply

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.

Continue reading →

Basics: Parallel, Concurrent, and Distributed

Leave a reply

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.

Continue reading →

An Experiment with π-calculus and Programming Language Design

Leave a reply

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.

Continue reading →

Backus's Idea of Functional Programming

Leave a reply

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.

Continue reading →

Sad News: John Backus has died.

Leave a reply

I just heard that John Backus died last saturday.

John Backus was one of the most influential people in the development of what we now know as software engineering. In the early days of his career, there was no such thing as a programming language: there was just the raw machine language of the hardware. Backus was the first person
to come up with the idea of designing a different language, one which was easier for
humans to read and write than machine code, and having the machine do the translation.

Continue reading →