6 posts tagged “π-calculus”

An Abstract Machine

Mar 12, 2009
Post a comment

I seem to have one. Here's the OCaml signature. The module file is all of 250 lines at this point, but I expect to define a lot of built-in processes for the preamble. That will bloat out the module file.

type 'a t
module Op: sig
val ( >>= ): 'a t -> ('a -> 'b t) -> 'b t
end
val return: 'a -> 'a t
val eval: unit t -> unit
type n
type repeat = Once | Always
val nil: unit t
val start: unit t -> unit t
val lambda: n t
val nu: n t
val fusion: n -> repeat -> n list -> unit t -> unit t
val v_void: n
val v_true: n
val v_false: n
val if_then_else: n -> unit t -> unit t -> unit t
type dio = D_in | D_out
val def: dio list -> (n array -> unit t) -> n t
val preamble: n Name.Map.t t

Basically, the abstract machine is a monad. I'll compile programs into an abstract syntax tree, then when the tree is pruned until it conforms to all the syntax and semantics invariants, I'll visit the nodes to compose a monad value. I'll execute the program by evaluating the monad. To say that it will not be fast is an understatement of Brobdingagian proportions. It will be simulating concurrency in a single thread of control, which will seem like a wide miss of the whole point. It will, however, allow me to experiment with higher-level language syntax and semantics for a while before I hit the next wall, where I expect I will need to write a byte code interpreter in C with POSIX threads to make further progress.

Toward An Abstract Syntax

Mar 9, 2009
Post a comment

I continue to noodle around with an abstract syntax for types in my internal language. (Sigh. This is taking forever.) Here's what I'm looking at now:

τ ::= α | ν⟨σ⟩ | λ(σ)

σ ::= ∀δ,σ | ∃α,σ | τ,σ | ϵ

δ ::= α | α = τ | α > τ

Explanation. A type (τ) is either a named type variable (α), or a channel type of shape (σ) with either λ- or ν- binding. A shape (σ) is a list of universal quantifications, existential quantifications and type declarations terminated by the shape terminator code (ϵ), i.e. a channel that carries no types or values has type ϵ. The universal quantification is enriched with flexible (>) and rigid (=) constraints.

Some syntactic sugar is useful. The trailing ϵ in a shape can be elided from the bracketed expression in a λ- or ν- type expression, i.e. ν⟨α,β,ε⟩ can be written ν⟨α,β⟩. If the shape of a channel type expression has only one term before the ε, then the brackets/parentheses may be elided, i.e. λ(α,ε) can be written λα.

I'm still going back and forth with myself over where the λ's and ν's belong.

Monads In The π-Calculus

Mar 9, 2009
Post a comment

While I was in the shower this morning, it occurred to me that I should make a note for myself about how monads work in the polyadic D-fusion calculus.

The type construction is simply a channel (να) for sending a value of the underlying type.
The unit function is a channel (να λ(λ(να))) for sending a value of the underlying type and receiving a responsive channel that carries the resulting monadic value.
The binding operation is a channel (να ν(να λ(λ(νβ)))) λ(λ(νβ))) for sending two values, 1) a monadic value of type α and 2) a channel for sending a value of the underlying type α and receiving a responsive channel that carries the resulting value of monadic type β; the binding operation channel also permits receiving a responsive channel that carries the resulting value of monadic type β.

Easy as cake.

Note: the process defined according to the type above for the binding operation always starts when both inputs are available. There are two possible optimizations here: one where the process begins immediately when the value of monadic type α becomes available and one that begins immediately when the bound channel becomes available. The description of these types is left as an exercise.

Update: I made some consistency errors in the first revision of this post, so I went back and edited it to correct errors.

Curried Actions In The Polyadic π-Calculus

Feb 28, 2009
Post a comment

When you're building a concurrent functional programming language around an internal language derived from the π-calculus, it's a known strategy [c.f. Pict, by Pierce and Turner] to allow applicative expressions to be used in the place of π-names in action prefixes. These are a kind of syntactic sugar that expand to a concurrent process that produces the result of function application on an ephemerally bound name that takes the place of the expression.

I've been thinking lately about how currying might work in this syntax. It's doable, but I'm not sure it can be done implicitly the way OCaml and Haskell do it, i.e. where it always makes sense for the programmer to use the curried syntax over the uncurried syntax, because A) it's more flexible and B) it's faster (the uncurried form involves more boxing).

In OCaml, you can define a function like this:

let f u : int -> int -> int =

printf "u=%u\n" u;

fun v -> u + v

When you call that function with a partial application of only one argument, as in let x : int -> int = f 5 in ..., the printf function is called and the result is a function object that adds 5 to its integer argument and returns the result without printing any further output.

I'm not sure how OCaml does this, but it does.

What I want is a similar thing in the D-fusion calculus [a derivative of the π-calculus I've mentioned previously]. I think it might be doable, but I haven't figured it out yet. It seems like the arrow type operator actually needs to be a constructor in the derived syntax. The core internal syntax needs to allow for various principle channel sorts to appear in the derived syntax as expressions involving the arrow operator.

In other words, consider this derived type expression for a binary function in two polymorphic types:

∀α β. α → β → α

It can be derived from two different internal language principle type expressions that can be used equivalently in functional expressions so long as the compiler keeps track of things properly:

A :: ⟦ ∀α β. να νβ λ⟦ λα ⟧⟧

B :: ⟦ ∀α. να λ⟦ ∀β. νβ λ⟦ λα ⟧⟧⟧

The type expression in A) means send two names, one of type α and the other of type β, and receive one name of type ⟦ λα ⟧ where the response will arrive. The type expression in B) means send one name of type α and receive a name of type ⟦ ∀β. νβ λ⟦ λα ⟧⟧ where to send another name of type β and receive a name where the response will arrive. A functional definition where B and A are not equivalent processes would need to be recorded in the compiled module in pretty much the same way that OCaml does its magic.

I need to figure out how to handle that. I think, but I'm not sure, that this is what goes on inside compile interface files in OCaml. The signature says 'a b. 'a -> 'b -> 'a, but the .cmi file says the moral equivalent of "here is the address for partial applications in one variable, and here is another address for full applications in both variables."

More Math Noodling

Feb 26, 2009
Post a comment

Last night, I think I figured out some important things about the π-calculus.

p1. I believe there is a monadic D-fusion calculus in which it is possible to elaborate the canonical polyadic version described in the paper by Boreale, Buscemi and Montanari. (I don't think this is particularly surprising.)

p2. I believe I can elaborate the monadic D-fusion calculus with Milner's π-calculus. (It's possible, though it seems unlikely, that this is a novel observation. Of course, it's also possible that I'm wrong, and I don't really understand the D-fusion calculus.)

p3. I suspect— though, I can't say I'm very confident— that I will soon have a sorted derivative of the polyadic D-fusion calculus (at least, the D-fusion calculus as I understand it) in which I may be able to elaborate ML^F as described in the paper by Botlan and Rémy. [This, I believe, would be a noteworthy achievement.]

Naturally, because I am just a simple-minded code-monkey and not a real mathematician, I'm pretty much incapable of publishing results in the conventional manner with any hope of them surviving peer review. Maybe, if I get some spare time today, I'll buy a download of MathType and start trying to write up my thoughts in something approaching the conventional format for such things. What's the worst that can happen? (Answer: I'll be branded as a kook.)

Update: Ah, I see where I went wrong in p2 now. I forgot how the D-fusion calculus really is strictly more expressive than Milner's π-calculus because the scope of λ-bound variables can be weakened via the λ- OP E N rules. Okay, now I'm back on track.

Your Friends, The Actor Model and The π-Calculus

Feb 4, 2008
Post a comment

Just a brief note to go on the record. I note that the widespread deployment of pseudo-symmetric multiprocessing hardware in personal computers is giving software developers new reasons to put more energy into crawling up the concurrent programming learning curve. Sadly, it seems that a lot of the sooper-hip cool kids are glomming onto the latest craze in the world of haute couture for coders, i.e. The Actor Model.

I've been around this block. A lot. Kids, there is a reason we call them Computer Scientists. They actually do Science, not that buzzphrase-laden eXtreme Agility Kode-Monkee-Fu On Rails you're all excited about. Want to know how you can tell the difference? When they find a model that works better than their old one, they throw out the old one and use the new one. Then— and this is important— they publish their results, and remember not to use the old model when the new one is better.

Science. It works, bitches.

The "actor model" sounds new, right? Sorry. No, it's already outdated. What you want is a model more like The π-Calculus. Trust me on this one. Sure, it might mean having to learn a programming language that can be compiled into machine instruction code, but those are the little prices we have to pay to stay current with the literature. Deal.