Pattern Calculus

[Bernie Pope]

Hi all,

Barry Jay has published a new book on the Pattern Calculus:

http://www.springer.com/computer/foundations/book/978-3-540-89184-0

It may be of interest to some on this list.

Here is part of the blurb:

"The pattern calculus is a new foundation for computation, in which
the expressive power of functions and of data structures are combined
within pattern-matching functions. The best existing foundations focus
on either functions, as in the lambda-calculus, or on data structures,
as in Turing machines, or on compromises involving both, as in object-
orientation. By contrast, a small typed pattern calculus is able to
support all the main programming styles, including functional,
imperative, object-oriented and query-based styles, and there is
evidence that it can support a language for Web services, able to
exploit data structures about which almost nothing is known."

Cheers,
Bernie.

[Ben Horsfall]

On Mon, Nov 30, 2009 at 1:20 AM, Bernie Pope <bj...@csse.unimelb.edu.au> wrote:
> Barry Jay has published a new book on the Pattern Calculus:

I have the library's copy at the moment.


Ben

[canadaduane]

Hello all,

I'd like to thank Bernie for suggesting I join this forum to discuss
Pattern Calculus. I sent out a short message on the Haskell Cafe list
to see if anyone was reading and discussing the book.

So I have many questions, but as I read the book, one of the most
pressing is the following: how do you read and pronounce the symbolic
notation?

For example when you see a "case" arrow, my best-fit wording for "p --
> t" is "p chooses t". I suppose it could just as well be "p results
in t" or "when p then t".

One bit of notation that is still a little tricky for me to understand
is the {u / x} term substitution. How do you read this notation? Is
it "u becomes x"?

Thanks!
Duane

[Bernie Pope]

On 10/12/2009, at 12:30 AM, canadaduane wrote:

> So I have many questions, but as I read the book, one of the most
> pressing is the following: how do you read and pronounce the symbolic
> notation?

I don't have a copy of the book yet (it is on order), but I have read
parts of it from books.google.com.au.

>
> For example when you see a "case" arrow, my best-fit wording for "p --
>> t" is "p chooses t". I suppose it could just as well be "p results
> in t" or "when p then t".

I don't know about that one. Do you have a page reference?

>
> One bit of notation that is still a little tricky for me to understand
> is the {u / x} term substitution. How do you read this notation? Is
> it "u becomes x"?

I read "{ u / x }" as "substitute u for x".

Or equivalently, "replace x with u".

I think Barry says something like "x maps to u".

With substitutions you have to be careful to only replace free
occurrences of a variable, hence the discussion on pages 16 and 17.

For background reading, I really like Peter Sellinger's lecture notes
on the lambda calculus:

http://www.mscs.dal.ca/~selinger/papers/lambdanotes.pdf

See page 14 (sec 2.3) for a discussion of substitution. (Note: I think
Peter writes: M { x / y }, whereas Barry writes { x / y } M, the
difference being whether application of the substitution function is
written prefix or postfix).

Cheers,
Bernie.

[canadaduane]

Thanks for your thoughts & feedback, Bernie. The google groups parser
apparently chewed up my arrow and made it look like a quoted line of
text. Anyway, I think you got the gist of it.

The "case" notation starts primarily in chapter 4 with the static
matching pattern calculus (p. 34). It continues throughout the rest
of the book. For example, the static pattern calculus term syntax:

t ::= (term)
x (variable)
c (constructor)
t t (application)
p [arrow] t (case).

Replace an actual short right arrow for the [arrow] text.

Below that term syntax, Barry says "A case p [arrow] s has pattern p
and body s". I'm curious what other words should be used to
pronounce the notation.

Duane

[Bernie Pope]

Until you asked, I'd never thought about how to pronounce the case
construct, but it is a good question.

It looks like the case construct subsumes something that we already
have in Haskell (and similar languages), namely the lambda expression,
eg:

\ (x : xs) -> x

How do you pronounce that? (I don't have a good answer).

But getting back to the pattern calculus "p -> t", some of the ideas
you suggested sound reasonable to me, especially "when p then t".

I'd like to emphasise the matching that happens in p, so perhaps
"match p yielding t"?

I guess we could always ask Barry how he pronounces it, but maybe we
can wait until we have a bunch of questions to ask, and send them as a
batch.

As an aside, I think it is nice if authors do suggest ways to
pronounce their notation, especially if it is not conventional
notation, and I will try to keep this in mind for future writing.

Cheers,
Bernie.

> --
> To unsubscribe from this group, send email to fpunion-u...@googlegroups.com

[Bernie Pope]

Hi,

I've posted my slides from Friday's talk on the (static) pattern calculus:

http://ww2.cs.mu.oz.au/~bjpop/slides/static_pattern_calculus.pdf

Haskell code for my interpreter for the static pattern calculus is available on patch tag:

http://patch-tag.com/r/bjpop/static-pattern-calculus

You can browse the code online, or download it with darcs:

darcs get http://patch-tag.com/r/bjpop/static-pattern-calculus

Cheers,
Bernie.

[Bernie Pope]

Some more remarks about the pattern calculus, in particular the dynamic calculus, arising from Friday's talk.

Here is the syntax of the dynamic pattern calculus (page 47):

t ::=
x (variable)
x^ (matchable symbol)
t t (application)
[theta] t -> t (case)

There are several notable aspects of the language:
- Patterns and terms are identified (now they belong to the same syntactic class).
- Data constructors are gone.
- Matchable symbols are distinguished from variables (matchable symbols have a "hat" above them like so: x^)
- The left hand side of a case contains a term, which effectively means that "patterns" can be computed.
- Binding occurrences of variables are indicated by [theta], which is attached to case terms.

Two things in the language are entirely conventional:
1) Variables behave as they always do; they undergo substitution during reduction. What makes them slightly more interesting is that they can now appear inside the "pattern" part of a case.
2) Term application hasn't changed.

The most unusual aspect of the language is the matchable symbols. In the static calculus the matchable symbols behave in a straightforward way, more-or-less in the same way that pattern variables behave in Haskell. The only real difference between the static pattern calculus and Haskell is that the former allows the head of a compound pattern to be a matchable symbol, whereas the latter requires it to be a constructor. In the dynamic pattern calculus matchable symbols are first-class terms, and as such they can be involved in reductions.

On page 46 Barry makes several remarks about the difference between variables and matchable symbols. He points out that matchable symbols really have two roles to play: 1) matching and 2) binding. The big issue to address is that reduction in a pattern can eliminate occurrences of matchable symbols. This is a potential problem if the eliminated symbols are also treated as binding occurrences of variables. That is to say, the scope of a variable/symbol would become a dynamic property of the program, rather than a static property. He says "That is, bindings must be static, even though patterns are dynamic". Unfortunately he doesn't say /why/ bindings must be static (except for the problem of dynamic scope). Of course dynamic scope is generally frowned upon today, nevertheless I think there is a missing justification that should have been said. To make bindings static he requires that binding occurrences of variables are annotated by [theta] on case terms.

Curiously the matchable symbols which do not appear in binding positions act just like data constructors, and so they play that role too (and data constructors are no longer needed as a separate entity).

Cheers,
Bernie.