Thursday, 11 December 2008

Equality, containment and intersection among regular expressions via symbolic manipulation

Three standard regular expression operations

data RE a where
Phi :: RE a -- empty language
Empty :: RE a -- empty word
L :: a -> RE a -- single letter taken from alphabet a
Choice :: RE a -> RE a -> RE a -- r1 + r2
Seq :: RE a -> RE a -> RE a -- (r1,r2)
Star :: RE a -> RE a -- r*
deriving Eq

equality :: Eq a => RE a -> RE a -> Bool
intersect :: Eq a => RE a -> RE a -> RE a
contains :: Eq a => RE a -> RE a -> Bool

implemented via symbolic manipulation of regular expressions (no explicit finite automata construction) by adapting Antimirov's regular expression rewriting algorithm via partial derivatives.

The implementation is available via the Haskell platform hackage. Check out the regexpr-symbolic package.

The source code describes some of the technical details. You can also check out an earlier post which considers the specific case of intersection.

Saturday, 6 December 2008

Parallel Join Patterns with Guards and Propagation

A paper in the works for quite some time. You can download the latest version here.

Here's what the abstract says:
Join patterns are a powerful concurrency abstraction to coordinate multiple events. We propose an extension with guards and propagation and argue that both features are essential in many programming situations. We develop a parallel execution scheme which we have fully implemented as a library in Haskell. Our results provide new insights how to write parallel programs on multi-core architectures.

Interested? You can get the implementation via the Haskell platform hackage. Download the join package which in turn relies on the multisetrewrite package. The multisetrewrite package provides the basic functionality to execute join patterns (with guards and propagation) in parallel. The join package adds synchronous and asynchronous arguments and join method calls. The user interface is still a bit clumsy to use but this will hopefully be improved over time.

Friday, 5 December 2008

Concurrent Goal-Based Execution of Constraint Handling Rules

We (my PhD student Edmund and me) have just submitted a paper with this title to Theory and Practice of Logic Programming. The paper complements our PPDP'08 paper on parallel Constraint Handling Rules execution. You can get the paper here.

Here's what the abstract says:
We introduce a systematic, concurrent execution scheme for Constraint Handling Rules (CHR) based on a previously proposed goal-based CHR semantics. We establish strong correspondence results to the abstract CHR semantics, thus guaranteeing that any answer in the concurrent, goal-based CHR semantics is reproducible in the abstract CHR semantics. Our work provides the foundation to obtain efficient, parallel CHR execution schemes.

Thursday, 4 December 2008

STM with control: Communication for retrying transactions

While working on the join pattern with guards and propagation implementation, we (my PhD student Edmund and me) came across an interesting problem which points out the current limited control/communication capabilities of retrying STM transactions (in Haskell). More on join patterns later. Here's the gist of the problem and a solution in form of a new Haskell library.

The task



We're given a list of switches, they can either be on or off


> data Switch = On | Off


If all switches are on, we switch them all off and report True If one switch is off, we do nothing and report False.

In a sequential setting, this task is straightforward. But what if the switches are shared among concurrent threads performing the above task?

In a concurrent setting, the task must be formulated as follows.

Atomically (
If all switches are on, we switch them all off and report True
If one switch is off, we do nothing and report False. )

Sounds like an application of STM. Indeed, here's a solution.


> verifyAndSwitchOff :: [TVar Switch] -> IO Bool
> verifyAndSwitchOff ts =
> atomically $ do
> bs <- mapM (\s -> do v <- readTVar s
> case v of
> On -> return True
> Off -> return False)
> ts
>
> if (and bs)
> then do mapM (\s -> do writeTVar s Off) ts
> return True
> else return False



We first check that all switches are on. Only then we switch all of them off. Isolation and atomicity of STM are important here.

Isolation guarantees that no intermediate step is visible to any other thread. After checking that all switches are on, we have the guarantee that they are still on, once we switch them off. Atomicity guarantees that all operations are executed all at once or not all which implies that some of the initially read switch values has changed. In this case, we abort the transaction and discard all changes so far and start over again.


It's tempting to immediately turn a switch off once we've read that the switch is on. But what if we read that a switch is still on? We need some additionally functionality to explicitly abort the transactions. That's what the retry and orElse combinators are for.


> verifyAndSwitchOff2 :: [TVar Switch] -> IO Bool
> verifyAndSwitchOff2 ts =
> let loop [] = return True
> loop (s:xs) = do v <- readTVar s
> case v of
> On -> do writeTVar s Off
> loop xs
> Off -> return False
> in atomically $
> (do b <- loop ts
> if b then return True
> else retry)
>
> `orElse`
>
> return False


The loop reads the status of each switch and turns the switch off if the switch is on. Otherwise, we 'abort' by returning False. For example, in case of the initial list [On, On, Off, On] we reach the third switch and the intermediate result [Off, Off, Off, On]. We can't just naively exit at this stage because the tasks demands that all changes are done atomically, ie to its full extent or not at all.

Here comes the rescue. The retry combinator allows the programmer to explicitly abort a transaction. That is, we discard all changes (which is important) here. The orElse combinator allows the programmer to compose two transaction. The second transaction will be executed if the first transaction retries. Exactly what we require.

Making the task more interesting



Suppose each switch is attached to an action, sort of a continuation. Let's say an IO action.


> type Cnt = IO ()


We want to return the continuation of the switch which first 'failed'. Here's the updated task description.

Atomically (
If all switches are on, we switch them all off and report True
Otherwise, return the continuation of the first turned on switch.)

The signature of the function we need to implement


verifyAndSwitchOffCnt :: [(TVar Switch, Cnt)] -> IO Cnt


What are our options how to implement the above?

We could adapt our first solution verifyAndSwitchOff. This is pretty straightforward. What about verifyAndSwitchOff2? Previously, we simply return False in the second orElse branch. For the more interesting task, we need to iterate over the list of pairs of switches and continuation and select the continuation of the first switch which is still on. This means that in both case we possibly need to iterate over the list twice. This is inefficient and leads to clumsy code.

Below we make use of an extension of STM where a retrying transaction can pass some information to the second transaction composed with orElse.

The extension is implemented as the STMControl.STMC library. The new primitives are:


newTVarC :: b -> STMC a (TVar b)
readTVarC :: TVar b -> STMC a b
writeTVarC :: TVar b -> b -> STMC a ()
atomicallyC :: STMC a b -> IO b
retryC :: a -> STMC a b
orElseC :: STMC a b -> (a -> STMC a b) -> STMC a b



STMC stands for STM with more control. The first parameter refers to the type of the value transmited in case of a retryC. The parameter in the orElseC combinator is now a function which accepts the result transmitted of the retrying transaction.

The implementation is fairly simple and uses an (abused) reader monad on top of STM. Here's finally an application of the new functionality.


> verifyAndSwitchOffCnt :: [(TVar Switch, Cnt)] -> IO Cnt
> verifyAndSwitchOffCnt tcs =
> let loop [] = return Nothing
> loop ((s,c):xs) = do v <- readTVarC s
> case v of
> On -> do writeTVarC s Off
> loop xs
> Off -> return (Just c)
> in atomicallyC $
> (do r <- loop tcs
> case r of
> Nothing -> return (return ()) -- default (donothing) continuation
> Just c -> retryC c)
>
> `orElseC`
>
> (\c -> return c)


The loop checks and resets all switches. In case a switch is turned off we return the attached continuation. We use the Maybe type to indicate failure (Just c) or success (Nothing). In case of success, we return the donothing continuation. Otherwise, we retryC to discard all changes made so far and pass the continuation to the second transaction which then returns this continuation.

I'd say compared to the other options, the STMC solution looks pretty clean and easy to understand.

Making the task even more interesting



That's the final extension, I promise. Suppose that to each switch there's also an attached STM Bool transaction. In addition to testing that the switch is off, we also test that the STM Bool transaction evaluates to True. Otherwise, we discard our changes and return the attached continuation.


> verifyAndSwitchOffCnt2 :: [(TVar Switch, STM Bool, Cnt)] -> IO Cnt
> verifyAndSwitchOffCnt2 tcs =
> let loop [] = return Nothing
> loop ((s,stm,c):xs) =
> do v <- readTVarC s
> case v of
> On -> do writeTVarC s Off
> b <- lift $ stm

STMC are (reader monad) lifted STM operations

> if b then loop xs
> else return (Just c)
> Off -> return (Just c)
> in atomicallyC $
> (do r <- loop tcs
> case r of
> Nothing -> return (return ()) -- default (donothing) continuation
> Just c -> retryC c)
>
> `orElseC`
>
> (\c -> return c)


The required changes to our previous solution are minor. In fact, I can't see how to implement the even more interesting task with STM alone. I believe that this task strictly requires STMC or something similar.


The complete source code of this example is available as part of the stmcontrol package on the Haskell platform hackage.

Implementation details




type STMC a b = ReaderT (IORef a) STM b

retryC :: a -> STMC a b
retryC x = do msgChan <- ask
lift $ unsafeIOToSTM (writeIORef msgChan x) -- L1
lift $ retry


What if the transaction is aborted just after execution of L1? Is our use of unsafeIOToSTM (un)safe? It's safe. It's okay to discard the IO action in case the transaction is rolled back. The important point is that if the transaction is explicitly retried, the IO action has been executed (which is the case as far as I understand the interplay of STM and unsafeIOToSTM).

Monday, 1 December 2008

XHaskell

My PhD student Kenny has just submitted his thesis on XHaskell - Adding Regular Expression Type to Haskell.

You can download the latest XHaskell implementation and Kenny's thesis draft here

Saturday, 29 November 2008

Transactions in Constraint Handling Rules

A paper to be presented at ICLP'08, Udine, Italy, December'08. My co-author Tom Schrijvers will give the presentation but here's already a draft of the talk.

If you've followed my previous posts on (software) transactions (in memory aka STM), this paper is more on the theoretical (greek symbol) side, but still worth a read if you seek for a systematic method to improve the efficiency of your STM code.

In the paper, we enrich the Constraint Handling Rules (CHR) calculus with transactions. If you've never heard the name CHR before, think of multi-set rewriting, bounded transactions, or a form of join pattern with guards and propagation. The paper develops a theory of how to (possibly) transform unbounded transactions to bounded transactions. Under optimistic concurrency control, unbounded transactions (e.g. transactions traversing a dynamic data structure such as a linked list) often yield "false" conflicts which means that transactions are executed sequentially instead of in parallel. Bounded transactions (e.g. dining philosphers which grap a bounded, two, number of forks) are generally free of such (in)efficiency problems. Details are in the paper.

Tuesday, 18 November 2008

High-level Software Transaction Protocols

The topic is how to built high-level (composable) software transaction protocols on top of highly-concurrent, low-level data structures which are not composable. Yes, this is sort of a continuation of my previous 'Transactional Boosting' post. What I'm looking for is a systematic method to built boosted protocols. I believe that a promising formalism are join patterns (aka multi-set rewrite rules).


Transactional boosting revisited



Here's my attempt to recast the transactional boosting approach in terms of the join pattern language extension I'm currently working on. Join patterns can now have guards and propagation. For example, the following join patterns says

foo(x,y) \ bar(y,z) when x > z = ...

if we find method calls foo(x,y) and bar(y,z) where the condition x > z holds (notice the implicit constraint imposed via the shared variable z), then we remove (simplify) bar(y,z) from the method store but we keep (propagate) foo(x,y).

Okay, so let's make use of such join patterns to specify the boosted transactional protocol. For simplicity, let's consider a very simple to be boosted object. A set with one 'add' operation.


The interface:

add x = do t <- readEnv
r <- newSync
addI(t,x,r)
v <- readSync r


From the environment, we get the current transaction identifier (kind of ThreadId). We create a synchronization variable on which we will block. But first we call the method
addI(t,x,r) whose interaction with other method calls is specified below
(In a Join setting, method calls are recorded in a store).


The protocol to check for conflicts:

-- conflict --> suspend
addI(t1,x,_) \ addI(t2,x,r) = addS(t2,x,r)

-- commute
addI(t1,x,_) \ addI(t2,y,r) when x \= y = do primAdd y
register t2 'remove y'
r:= ()
addToStore 'addI(t,x,r)'

-- first call
addI(t,x,r) = do primAdd x
register t 'remove x'
r:= ()
addToStore 'addI(t,x,r)'


The first join pattern checks for non-commuting method calls (subtle point: we assume that the propagated head will NOT be executed as a goal). Join patterns are tried from top to bottom (in our implementation). Hence, if the first join pattern can't fire we try the second one which applies if all calls to add commute and there exist at least two add calls (we assume multi-set semantics, one call can't match two occurrences). In the 'commute' case, we call the primitive add (relying on the highly-concurrent, low-level data structure) and unblock the original add call. Registering of the inverse operation is necessary in case we abort the transaction. The last join pattern applies if we're the first to call add. Adding add calls to the store guarantees that
all calls are made visible to each other.

A transaction can only commit (reach the end) if it doesn't encounter conflicts. Otherwise, the transaction will be suspended.

The commit protocol has two stages. We first unblock one suspended add call (if exists). Otherwise, we do nothing. The assumption is that the committing transaction calls 'commit(t)'.

commit(t), addI(t,x,_), addS(t2,x,r) = addI(t2,x,r)
commit(t) = return ()


Actually, we could be more optimistic and unblock all commuting add calls. I can't see how to nicely formulate this with join pattern alone (we'd need to traverse all suspended calls and select all commuting ones).

We yet to release all 'locks' (the stored add calls) held by transaction t. Once more, we call 'commit(t)'.

commit(t) \ addI(t,x,_) = return ()
commit(t) = return ()

The propagated goal 'commit(t)' guarantees that we exhaustively release all locks (a for loop join pattern style).

In the last commit step, we erase all registered inverse operations.

As said above, in the current formulation, a transaction can only reach the end (and thus commit) if it doesn't encounter conflicts. The transaction won't fail or retry. It can only happen that the transaction is suspended, possibly indefinitely.

To avoid 'cyclic suspension' deadlocks, the 'transactional boosting' approach uses a time-out to actually fail a transaction. In case of failure, we need to remove the transaction's method calls

fail(t) \ addI(t,_,_) = return ()
fail(t) \ addS(t,_,_) = return ()
fail(t) = return ()

and we execute the registered inverse operations. Then, the transaction is started from scratch.

Where to go next



The above description is not necessarily meant to be used in an efficient implementation. However, I believe that the use of join patterns allows us to to give a nice declarative specification of 'transactional boosting' and its underlying protocols. I will be interesting to consider alternative 'boosting' protocols. It appears that in general the 'boosting' approach can only support pessimistic concurrency. Optimistic concurrency requires that a transaction only commits its updates only after no conflicts have been detected.

In my experience, transactional boosting and optimistic concurrency only works out for some specific cases, eg the multi-set rewrite stuff I mentioned in my earlier 'Transactional Boosting' post.

Anyway, there's still lots to discover. Guess that's something for a future post.

Sunday, 16 November 2008

Transactional boosting

This post is about software transactional memory (STM) and how to retain its benefits (composability) while trying to minimize its drawbacks (poor performance due to false conflicts).

Software transactional memory: Composability and false conflicts



Software transactional memory (STM) is a concurrency control mechanism analogous to database transactions for controlling access to shared memory in concurrent computing (wikipedia). Below is a simple example of a concurrent, unordered singly-linked list using STM as supported by GHC Haskell.


date List a = Node {val :: a, next :: TVar a}
| Nil

insert :: TVar a -> a -> STM ()
find :: TVar a -> a -> STM Bool
-- True = present, False = absent
delete :: TVar a -> a -> STM Bool
-- True = present and deleted, False = absent

-- atomically delete 3 and 4 if present
transaction :: TVar a -> IO Bool
transaction root = atomically $ do
b1 <- find root 3
b2 <- find root 4
if b1 && b2 then do
delete root 3
delete root 4
else return False


The straightforward definitions of the linked list operations are left out. They are all executed within the STM monad which will guarantee that the operation is executed atomically, i.e. to its full extent or not at all which means in the programm language setting that we re-run (aka rollback/retry) the operation.

In Haskell, we can easily build 'bigger' STM operations by gluing together 'smaller' STM operations. For example, the transaction checks if elements 3 and 4 are present in the list and then will delete both elements. The entire transaction is executed atomically which guarantees that in case we return True, elements 3 and 4 were present but have now been deleted. Neat!

The benefits of STM over say locks are well documented. However, STM has (often) a significant performance disadvantage. Our (naive) STM implementation will protect the entire list. Suppose that elements 3 and 4 are stored towards the tail of the list. Hence, we (almost) need to traverse the entire list which then potentially leads to false conflicts with other concurrent STM operations. The effect is that many concurrent STM operations will be serialized (i.e.~sequential instead of parallel execution).

Comparing concurrent linked-list implementations in Haskell



I recently wrote a paper with the above title to be presented at DAMP'09, in collaboration with Simon Marlow and Edmund Lam. Our results show that the naive STM implementation is no match against more fine-tuned implementations which


  • either side-step the STM protocol (only each node operation is performed within the STM)
  • employ lock-coupling via Haskell's MVars, or
  • rely on atomic compare-and-swap.

Please check the paper for the details.

The (well-known) downside of this more efficient singly-linked operations (efficient in the sense they enjoy a higher degree of concurrency) is that they are not composable anymore. That is, it is non-trivial to implement the above transaction (atomically find and delete 3 and 4) using the more efficient implementations.

Transactional boosting



Maurice Herlihy and Eric Koskinen wrote two recent papers on a topic they refer to as transactional boosting: How to recover the 'high-level' benefits of STM while relying on 'low-level', highly concurrent data-structures.
The papers are (see Eric's website):

  • Transactional Boosting: A Methodology for Highly-Concurrent Transactional Objects
    M. Herlihy, E. Koskinen. PPoPP 2008
  • Aggressive Transactional Boosting
    E. Koskinen, M. Herlihy.
    Under submission. August 2008.


My understanding of how the transactional boosting approach meant to work is that


  • the user needs to verify if primitive operations 'commute', otherwise
  • the operands of (non-commuting) operations will be protected by an abstract lock,
  • each operations requires an inverse which will be executed if the transaction fails to commit.


It seems that the transactional boosting approach assumes pessimistic concurrency. I'm still not clear about the exact details of the approach but it looks definitely very promising.

Incidentally, I ran across the issue of transactional boosting in my own work on concurrent execution of multi-set rewrite rules.

Multi-set rewriting and transactional boosting



Below are simple examples of (monomorphic for simplicity) multi-set rewrite rules.
Right-hand sides are omitted because they don't matter here.

A, B <==> ...
A, C <==> ...


Multi-set rewrite rules operate on a store, a multi-set of elements. We can concurrently apply multi-set rewrite rules if they operate on non-conflict parts of the store. Suppose, we have the store

{A, A, B, C}

Then, the first rule can be applied on (the first) A and B and the second rule can be
applied on (the second A) and C. There's no conflict. Hence, both rules can be applied concurrently.

The point is that the store is implemented as a concurrent data-structure and execution of a rewrite rule can be viewed as an STM transaction. For example, the operational interpretation of the first rule is

atomically $ do
find A
find B
if both present
then do delete A
delete B
else return ()


The first implementation of concurrent multi-set rewrite rules, in collaboration with Edmund Lam (my PhD student btw), presented here

Edmund S. L. Lam, Martin Sulzmann:
A concurrent constraint handling rules implementation
in Haskell with software transactional memory. DAMP 2007:

used a (naive) STM list to implement the store. Our experiments confirm that such an approach won't scale. Due to a high(ly likely) number of false conflicts, multi-set rewrite rules are executed sequentially, though, we ought to execute them in parallel.

Our latest implementation, presented here

Martin Sulzmann, Edmund S. L. Lam:
Parallel execution of multi-set constraint rewrite
rules. PPDP 2008

uses a more low-level, 'more concurrent' data-structure which is *not* composable. Hence, we had to implement our own STM protocol on top of the low-level data-structure (The PPDP paper is a bit unclear about this but we'll present what we've achieved in its full glory in a forth-coming journal submission soon).

Summary



STM is great but it often has poor performance. There are many applications where we wish to have a 'transactional boosting' approach. As far as I can tell, the approach laid out by Maurice Herlihy and Eric Koskinen is fairly different from the approach we used for concurrent execution of multi-set rewrite rules. Possibly, there's some unifying theory but I have the feeling that transactional boosting relies on some domain-specific assumption. Anyway, interesting times with many interesting topics. I'm sure there' more to say about transactional boosting.

Wednesday, 12 November 2008

Actor versus Join Concurrency

This post tries to shed some light on the differences and commonalities between actor and join style concurrency and explains its connection to multi-set rewrite rules.

Recently, I've published two libraries supporting


  • Actor concurrency, see here, and
  • Join concurrency, see here


Coordination via multi-set rewrite rules with guards



Both libraries support similar forms of coordination primitives in terms of multi-set rewrite rules with guards. For example, consider

Seller x, Buyer x --> "do something"

which says that if there's a seller and a buyer where both agree on the object x to be sold, then we execute the right-hand side "do something".

What's the connection to rewrite rules? Well, in case there's "Seller Obj" and "Buyer Obj", both will be rewritten to "do something". It's natural to view sellers and buyers as resources. To rewrite multiple resources, we simply use multi-set rewrite rules. For example,

A, A --> "blah"

will remove two occurences of "A" by "blah".

Lesson learned so far. The basic coordination primitives behind actor and join style concurrency are expressed in terms of multi-set rewrite rules. In the join setting, these multi-set rewrite rules are commonly referred to as join-patterns. However, please take note that Erlang-style actors only support single-headed rewrite rules and join-style concurrency as found in JoCaml, Polyphonic C or Claudio Russo's Joins librariy does not support guards (both features are supported by the above mentioned libaries).

Assuming we agree on a common set of multi-set rewrite rules (possibly with guards), what's the difference then between actor and join concurrency?

Actor concurrency



In the actor setting, we commonly assume that multi-set rewrite are applied sequentially. In the special case of Erlang's single-headed rewrite rules, we start scanning the mailbox (that's the place where sellers, buyers etc are stored) from left to right. For each mailbox element (often referred to as message aka method or even constraint in the rewrite setting), we then try the single-headed rewrite rules from top to bottom, until a match is found. In the general case of multi-set (headed) rewrite rules, we can assume that things can get a bit more tricky. Check out the paper below for a formal sequential execution semantics

Martin Sulzmann, Edmund S. L. Lam, Peter Van Weert,
Actors with Multi-headed Message Receive Patterns.
COORDINATION 2008

But if rewrite rules are executed sequentially where does concurrency come in? Well, we can have concurrent actors which communicate by sending each other messages (aka methods or constraints). The messages itself are processed and executed sequentially by each actor. You may therefore argue that the behavior of each actor is completely deterministic.

Join concurrency



In the join setting, the place where methods (aka messages or constraints) are kept is commonly referred to as a "store". Any multi-set rewrite rule can fire as soon as we find a match for its left-hand side among the st of stored methods. The only condition is that if two rewrite rules fire concurrently, they must operate on non-overlapping parts.

Summary



Both styles of concurrency use the same coordination primitive, i.e. multi-set rewrite rules. I'd argue that actor and join concurrency serve different purposes (hence, are equally useful). One can emulate the other but I prefer to have efficient support for both of them (not via emulation).

NOTE: I wrote this post are seeing these comments on reddit.com:

So, having a blog is possibly useful after all :)

The BaggerProblem

Description



There are n number of bags which can be filled up with either large, medium or small items. The weight of items of a specific kind is fixed. The maximum weight carried by a bag is fixed.

Bags are filled up with items in a fixed order:

  • 1. In sequential order from lowest to highest bag number
  • 2. Exhaustively fill up the bag first with

    • (a) large items, then
    • (b) medium items, then
    • (c) small items.



The straightforward solution is to

  • 1. Fill up bags with large items, then
  • 2. with medium items, and then finally with
  • 3. small items.


However, once a bag has been exhaustively filled up with large items (we either stop because the bag reached its maximum capacity of large items, or we're simply running out of large items), we can start filling up this bag with medium items. The point is that we don't have to wait until all bags are exhaustively filled up with large items.

This form of concurrency has clear connection to instruction pipelining. What we want to show here is how to come up with a concurrent solution to the bagger problem

We'll give two solutions:


  • a solution using join-patterns extended with guards,
  • from which we can easily derive a more 'elementary' solution using standard synchronization primitives such as Software Transactional Memory (STM).


Solution using Join extended with guards



The join-calculus (and languages implementing join-patterns) doesn't support guards. Hence, we make use of our join extension which supports guards. The guards we use here are in fact implicit (shared variables). Here we go:


The methods we introduce are:

Bag(kind,no,content) denotes a bag which

- currently expects to be filled with items of kind 'kind'
- no is the bags number
- content refers to the current content

Initially, all bags are of the form

Bag(Large,i,Empty)


Item(k) denotes an item of kind 'kind'


The above methods are all asynchronous.

We introduce two synchronous methods.

Iterator(kind,no) fills up bag number no with items of kind 'kind'.
Initially, there are three 'iterators':

- Iterator(Large,1)
- Iterator(Medium,1)
- Iterator(Small,1)

Each will run in its own thread. Each starts in 'Large' mode.
That is, only the large iterator can fill up the bags (sequentially).
Once the large iterator is done with bag number i, the bag is
'unlocked' by moving from 'Large' to 'Medium' mode and so on.

GetItem(kind,r) looks for an item of kind 'kind', the outcome
is reported in r of type Maybe Weight.

Here are the join patterns and their bodies.
(We assume that join patterns are executed from top to bottom,
for convenience only)

Bag(kind,no,content) & Iterator(kind,no) =
if (weight content) + (weight kind) >= maxBagWeight
then do bag (next kind) no content
if no < MaxBagNo
then iterator kind (no+1)
else return ()
else do
r <- getItem k
case r of
Nothing -> do
bag (next kind) no content
if no < MaxBagNo -- (***)
then iterator kind (no+1)
else return ()
Just itemWeight -> do
bag kind no (add content itemWeight)
iterator kind no


Item(k) & GetItem(k,x) = case k of
Large -> x := Just Large
...

GetItem(k,x) = x:= Nothing


NOTE:

First, I thought we could replace (***) by the 'default' rule

Iterator(kind, no) = return ()

which we put *after* the first rule.

However, this won't work because the 'small' iterator waiting for
the medium and large iterator may terminate prematurely.



A concrete implementation of the above can be found
here as part of the multisetrewrite library.

Elementary solution in Haskell using STM





> import IO
> import Data.IORef
> import Control.Concurrent
> import Control.Concurrent.STM
> import Control.Concurrent.Chan


We set up the item space by storing large, medium and small
items into their respective list. For each kind of items,
there's at most one thread trying to access the items.
Hence, using IORefs is fine.

> data ItemSpace = IS { large :: IORef [()]
> , medium :: IORef [()]
> , small :: IORef [()] }

We only store () values, the weights are fixed.

> largeWeight = 6
> mediumWeight = 4
> smallWeight = 2


The kind of items we support are either large, medium or small.
Done is a "dummy" item. We'll move from large to medium to small items.
Done simply indicates that we are done.

> data Item = Large | Medium | Small | Done deriving (Eq, Show)


> next :: Item -> Item
> next Large = Medium
> next Medium = Small
> next Small = Done

> itemWeight :: Item -> Int
> itemWeight Large = largeWeight
> itemWeight Medium = mediumWeight
> itemWeight Small = smallWeight


The procedure to fetch items. There may be concurrent threads
accessing either large, medium or small items. But there's
at most one thread for each kind.

> fetch :: ItemSpace -> Item -> IO (Maybe ())
> fetch is kind =
> let get m = do
> l <- readIORef m
> case l of
> (x:xs) -> do writeIORef m xs
> return (Just x)
> [] -> return Nothing
> in case kind of
> Large -> get (large is)
> Medium -> get (medium is)
> Small -> get (small is)


Each bag records its current weight and content.
The mode tells us which kind of items are currently allowed to
be put into the bag. The mode is protected by a TVar which allows us
to suspend until the large items are exhaustively put into the bag.

> data Bag = Bag { mode :: TVar Item
> , curWeight :: IORef Int
> , content :: IORef [Item] }

> printBag :: Bag -> IO ()
> printBag bag = do
> w <- readIORef (curWeight bag)
> c <- readIORef (content bag)
> putStrLn $ (show (w,c))

The maximum weight held by each bag is fixed.

> maxBagWeight = 16


We add an item to a bag by incrementing the bags weight
plus updating the content.

> add :: Bag -> Item -> IO ()
> add bag kind = do
> w <- readIORef (curWeight bag)
> c <- readIORef (content bag)
> writeIORef (curWeight bag) (w + itemWeight kind)
> writeIORef (content bag) (kind : c)


We check if a bag becomes full (over-weight) if we would add
another item.

> bagIsFull :: Bag -> Item -> IO (Bool)
> bagIsFull bag kind = do
> w <- readIORef (curWeight bag)
> return ((w + itemWeight kind) > maxBagWeight)



fillBag fills up (exhaustively) a bag with items of a given kind.
We 'unlock' the bag by 'incrementing' the mode if
- the bag is full
- no more items of this kind are left


> incrementMode :: Bag -> IO ()
> incrementMode bag =
> atomically $ do status <- readTVar (mode bag)
> writeTVar (mode bag) (next status)

> fillBag :: ItemSpace -> Bag -> Item -> IO ()
> fillBag is bag Done = error "not happening here"
> fillBag is bag kind =
> let loop = do
> b <- bagIsFull bag kind
> if b then incrementMode bag
> else do
> r <- fetch is kind
> case r of
> Nothing -> incrementMode bag
> Just _ -> do add bag kind
> loop
> in loop


We process (ie fill up) the list of bags sequentially.
For each bag we must wait untill its our turn.
The priorities are

large > medium > small


> waitMode :: Bag -> Item -> IO ()
> waitMode bag kind =
> atomically $ do status <- readTVar (mode bag)
> if status == kind then return ()
> else retry

> processBags :: ItemSpace -> Item -> [Bag] -> IO ()
> processBags is kind bs =
> mapM_ (\b -> do waitMode b kind
> fillBag is b kind) bs


For each kind we spawn a thread to fill up the list of bags.


> start :: ItemSpace -> [Bag] -> IO ()
> start is bs = do
> cnt <- atomically $ newTVar 0
> let spawn = \kind -> forkIO (do processBags is kind bs
> atomically $ do v <- readTVar cnt
> writeTVar cnt (v+1))
> spawn Large
> spawn Medium
> spawn Small
> atomically $ do v <- readTVar cnt
> if v == 3 then return ()
> else retry




testing

> createIS ln mn sn = do
> l <- newIORef [ () | x <- [1..ln]]
> m <- newIORef [ () | x <- [1..mn]]
> s <- newIORef [ () | x <- [1..sn]]
> return (IS {large = l, medium = m, small = s})

> emptyBag = do
> m <- atomically $ newTVar Large
> w <- newIORef 0
> c <- newIORef []
> return Bag {mode = m, curWeight = w, content = c}

> test largeNo medNo smallNo bagNo = do
> is <- createIS largeNo medNo smallNo
> bs <- mapM (\_ -> emptyBag) [1..bagNo]
> mapM_ (\b -> printBag b) bs
> putStrLn "Start"
> start is bs
> putStrLn "Done"
> mapM_ (\b -> printBag b) bs


Some observations



The STM solution can be improved. The thread filling up bags with large items doesn't need to check the status of the bag and the thread filling up small items only needs to be waken up once the 'medium' thread is done. We could achieve this behavior by replacing

mode :: TVar Item

with

mode1 :: TVar Item
mode2 :: TVar Item

That is, the 'medium' thread retries on mode1 and the 'small' thread retries on mode2.

In the join solution none of these optimizations are necessary, they are dealt with implicitly. For example, if Iterator(Small,someNo) is unable to fire a join-pattern, this method will be suspended (i.e. the method is put into the store). If the mode of a bag finally switches to small, this active bag will then in combination with the inactive (ie suspended) Iterator(Small,someNo) trigger the join-pattern.

Thursday, 6 November 2008

Gossiping girls

In my class on UPPAAL (a modeling and analysis tool for communicating FAs aka CFAs), I gave the following (classic) exercise:

A number of girls initially know one distinct secret each. Each girl has access to a phone which can be used to call another girl to share their secrets. Each time two girls talk to each other they always exchange all secrets with each other (thus after the phone call they both know all secrets they knew together before the phone call). The girls can communicate only in pairs (no conference calls) but it is possible that different pairs of girls talk concurrently.

Sounds like fun, right? Before, I discuss a sample solution in UPPAAL, let's consider some alternative frameworks which we could use to code up the above problem.

Here's a solution using CHR (Constraint Handling Rules):

Girl(name1,secrets1), Girl(name2,secrets2) <==>
newSecrets(secrets1,secrets1) | let s=shareSecrets(secrets1,secrets2)
in Girl(name1,s)
Girl(name2,s)


What about using Join-patterns extended with guards and synchronous method calls:

Girl(name1,secrets1) & Girl(name,secrets2) = do
secrets1 := secrets1 `union` secrets2
secrets2 := secrets2 `union` secrets2


Okay, so finally my UPPAAL solution. First, the declarations plus description. The actual CFA is displayed below.



// =========================
// == Global declarations ==

// We introduce two channels. First, I thought we can do with just
// one channel but then I believe things will get really messy.

chan call, call2;

// We assume that there are three secrets: one, two and three

// To pass secrets among girls we introduce three (global) variables,
// one for each secret.
// The value 0 indicates that the secret is not present (ie known).
// The value 1 indicates that the secret is known.

int var_s1, var_s2, var_s3;

// The actual transmission of values is performed in two steps:
// 1. First the caller tranfers her secrets
// 2. Then, it's the callee's turn to transfer her secrets.
// We must guarantee that this step happens atomically between
// two parties. We can either (a) use the UPPAAL feature of
// committed locations or (b) we simply transmit the callers identity
// which then the callee transmits back for verification.
// Option (a) sounds too easy, almost cheating :),
// so we'll pursue option (b).

// To transmit the callers identity, we'll need another "message-passing" variable.

int var_id;

// WARNING: We use here the initial_secret as a unique identifier
// which implies that we only supports girls which initially now
// a distinct secret.

// Please check the declarations of the girl template which
// describes the ideas and functionality of the CFA.




// =======================================
// == Declarations of the girl template ==

// Three variables to represent the girl's knowledge/status about
// the three secrets.

// We will initialize the variables when instantiating
// the girl template. The input parameter initial_secret
// refers to the secret that's initially known.

int s1, s2, s3;

// local variables to store the transmitted messages (secrets and caller id)

int in1, in2, in3, in_id;

// The first step of the girl CFA is to record (locally) the initially known
// secret. View as programming if-then-else statements using CFA transitions.
// If initial_secret == 1 then s1 = 1, s2 = 0, s3 = 0
// else and so on

// It gets interesting once we reach the "Start" state.
// In the first stage, we can either make a call, via "call!", or receive a call via "call?".
// In case we're the caller, we transmit our secrets and our identity (in form of the
// initial_secret). In case we're the receiver of the call, we're storing the
// transmitted values. Then, in the second stage, the roles switch and the caller
// becomes the receive and vice versa. Notice the use of a different channel.
// This is to avoid that a caller of the first stage can interact with a receiver
// of the second stage. We yet need to check that the caller and receiver of the
// first stage are still the same for the second stage. We perform this check
// in state "Verify" by comparing the transmited identify with our own (the initial_secret).
// A point to note is that this check is only performed by the receiver
// of the second stage.
// States "Update_Secrets1" and "Update_Secrets2" then update the secrets after the
// exchange. The formula (x+y) - (x*y) evaluates to 1 or 0 for values 0 and 1.
// Sure, this could be done smarter using bit operations or simply using UPPAAL's
// C-style array.



// =========================
// == System declarations ==

girl1 = Girl(1);
girl2 = Girl(2);
girl3 = Girl(3);

// List one or more processes to be composed into a system.
system girl1, girl2, girl3;


And finally the CFA:
Girl
Get your own at Scribd or explore others:


So, which solution do you prefer? To be fair, UPPAAL is not meant for programming, it has its strength in analyzing CFAs via its expressive query language and model checker.

Wednesday, 5 November 2008

From Join to UPPAAL and back

I'm currently teaching a course using UPPAAL for modelling and anlysis of communicating FAs (finite automatas). In this post, I will show some interesting connections between communicating FAs and coordination patters as found in the Join calculus (referred to as Join for brevity).

For concreteness, let's consider a (classic) coordination example: The 'bridge' problem. We have four soldiers on the left (unsafe) side of the bridge. They'd like to cross the bridge to get to the right (safe) side. The problem is it's at night and they need a torch to cross the bridge. The torch can carry a maximum of two soliders. We assume that the torch always carries two soliders from right to left and only solider goes back (left to right).

In Join, we can specify/model this problem as follows. We introduce synchronous methods 'take', 'release' and 'takeBack' to model the actions. We introduce asynchronous methods 'free', 'one', 'two', 'oneLeft', 'rightSide' and 'oneFrom' to represent the states of the torch and 'unsafe(i)', 'towards(i)', 'safe(i)' and 'back(i)' to represent the states of soldier i. Their meaning will become clear once see the join-patterns describing the interaction between torch and soldiers.

The behavior of the torch is specified via the following join-patterns (using Haskell-style syntax).

free = do take
one

one = do take
two

two = do release
oneLeft

oneLeft = do release
rightSide

rightSide = do takeBack
oneFrom

oneFrom = do release
free


Of course, we could have unfolded the above definitions into the following (and thus omitting the intermediate states)


free = do take
take
release
release
takeBack
release
free

This makes it even clearer that the torch waits for two soldiers to grab the torch. Then, the torch (with the soldiers) crosses the bridge (this is implicit). The torch releases both soliders and the torch will take back a soldier and release this soldier on the unsafe side again. The more verbose representation (using the intermediate states) will be useful later when discussing the connection to communicating FAs.

We yet need to model the behavior of solider(i). We finally make use of some multi-headed join-patterns.

unsafe(i) & take = towards(i)

towards(i) & release = safe(i)

safe(i) & takeBack = back(i)

back(i) & release = unsafe(i)


For example, the first join-pattern above says that if solider i is in the unsafe state and we can take the torch, then we unblock the caller of take (remember that take is synchronous) and we issue a new asynchronous method call towards(i). The semantics of join-pattern is actually fairly simply. In essence, multi-set rewriting where the methods are treated as resources. The multisetrewrite library introduced in a previous post, can easily encode join-patterns (and even more, eg guards etc).
I will release some runnable code at some later stage.

The point of this exercise is not to show what can be done with Join, rather, we want to establish some connections to communicating FAs. So, what's the connection? In Join, a join-pattern is triggered (aka executed) if we can match the pattern head with the specified method calls. In communicating FAs, two automatas 'communicate' if we find matching send (!) and receive (?) transitions.


p --- a! --> q r --- a? --> t

-----------------------------------------

(p,r) --- a --> (q,t)


Each component of the tuple corresponds to the states of a communicating FA (CFA). If one CFA has a send edge (a!) which matches the receiving edge (a?) of another CFA, then we make a transition along those edges as shown in the above diagram. This smells similar to Join, right? Indeed, in Join we can represent

p --- a! --> q

by

p = do a
q

and

p --- a? --> q

by

p & a = q

The states are turned into asynchronous method calls and the actions 'a' are turned into synchronous method calls.


In fact, the Join program shown above was derived from the following CFAs
using this translation scheme.

The torch CFA:

Torch
Get your own at Scribd or explore others:


The soldier CFA:
Soldier 3
Get your own at Scribd or explore others:


It's also possible to systematically translate Join programs to CFAs but it's getting more tedious to work out the details. Both languages are equally expressive. However, (I claim) Join allows us to specify more complex coordination patterns more easily than CFAs (therefore the transformation to CFAs gets quite involved). The advantages of having a Join representation of CFAs is that we know how to efficiently execute Join programs (eg see the multisetrewrite library which exploits join-style concurrency by executing non-overlapping join-patterns in parallel). On the other hand, a CFA representation of Join allows to make use of UPPAAL's expressive query language and its model checking facilities. For example, via the query

E<> safe(1) and safe(2) and safe(3) and safe(4)

we can check if (assuming we have four soldiers) it's possible for all four soldiers to reach the safe side. E says there exists a trace and <> says there exists a state.

We can also check if the system does not deadlock

A[] not deadlock

This property is not satisfied for the following reason. In case all four soldiers are on the safe side and one solider makes its way back to the unsafe side, the soldier gets to the unsafe side but won't be able to get back to the safe side. Remember that in our torch model, we require two soldiers per torch. For this example at least, the deadlock property doesn't say much. We only know that the program will terminate (possibly in some undesired state).

UPPAAL's query language is a subset of CTL btw. This implies that we canNOT verify (very compliated) queries such as "are the join-patterns confluent". Confluence requires to quantify over traces, then over states and then again over traces which is beyond CTL (for good reasons because it gets way too complex to check such properties).

Anyway, the connection between Join and CFAs is quite useful. This way I became a much better UPPAAL user. First write your program in Join and then convert to CFAs. I will write more about this connection at some later stage.

Playing with regular expressions: Intersection

We implement symbolic intersection among regular expression
by adapting Antimirov's regular expression rewriting algorithm.
By symbolic we mean that regular expression are not transformed to
automata. We rewrite regular expressions by using partial derivatives.

The algorithm (highlights):


r1 `intersect` r2 =

let [l1,...,ln] = lettersOf (r1 | r2)
in

(l1, partDeriv r1 l1 `intersect` partDeriv r2 l1)
| ...
| (l1, partDeriv r1 ln `intersect` partDeriv r2 ln)


The idea is that each regular expression is turned into a
'disjunction' of clauses where each clause starts with
a letter, followed by the partial derivative of the regular
expression wrt that letter.

You probably will know Brzozowski's derivative operation
which says that


derivative r l = [ w | (l,w) in L(r) ]


If we would use derivatives the above algorithm
is non-terminating. For example,


deriv (Star (L 'A')) 'A'
--> <<>,'A'*>

deriv (deriv (Star (L 'A')) 'A') 'A'
--> (<{},'A'*>|<<>,'A'*>)


and so on. The nice property of partial derivatives is that
they are 'finite'. Each regular expression has a finite
number of partial derivatives. For example,


partDeriv (Star (L 'A')) 'A'

--> <<>,'A'*>

partDeriv (partDeriv (Star (L 'A')) 'A') 'A'
--> <<>,'A'*>


Please check the paper

Valentin M. Antimirov: Partial Derivatives of Regular Expressions and Finite Automaton Constructions.
Theor. Comput. Sci. 155(2): 291-319 (1996)

for more details on derivatives, partial derivatives and their connection
(roughly, derivatives correspond to DFA states and partial derivatives correspond to NFA states).


There's another source of non-termination which we explain via
the following example.


A* `intersect` A*

--> (A, A* `intersect` A*)


where we simplified partDeriv A* A --> <<>,A*> to A*

The point to note is that the proof tree is infinite. The standard approach
is to use co-induction which then yields a finite (recursive) proof.

OK, here's finally the Haskell implementation:


> {-# LANGUAGE GADTs #-}

We're just using the GADT syntax to write 'ordinary' algebraic data types

> module RegExpIntersection where

> import List


> data RE a where
> Phi :: RE a -- empty language
> Empty :: RE a -- empty word
> L :: a -> RE a -- single letter taken from alphabet a
> Choice :: RE a -> RE a -> RE a -- r1 + r2
> Seq :: RE a -> RE a -> RE a -- (r1,r2)
> Star :: RE a -> RE a -- r*
> Var :: Int -> RE a -- first-order variables to represent regular equations
> deriving Eq

A word is a list of alphabet letters

> type Word a = [a]

Pretty printing of regular expressions

> instance Show a => Show (RE a) where
> show Phi = "{}"
> show Empty = "<>"
> show (L c) = show c
> show (Choice r1 r2) = ("(" ++ show r1 ++ "|" ++ show r2 ++ ")")
> show (Seq r1 r2) = ("<" ++ show r1 ++ "," ++ show r2 ++ ">")
> show (Star r) = (show r ++ "*")

Turning a list of regular expressions into a regular expression by using | (choice)

> resToRE :: [RE a] -> RE a
> resToRE (r:res) = foldl Choice r res
> resToRE [] = Phi


Computing the set of letters of a regular expression

> sigmaRE :: Eq a => RE a -> [a]
> sigmaRE (L l) = [l]
> sigmaRE (Seq r1 r2) = nub ((sigmaRE r1) ++ (sigmaRE r2))
> sigmaRE (Choice r1 r2) = nub ((sigmaRE r1) ++ (sigmaRE r2))
> sigmaRE (Star r) = sigmaRE r
> sigmaRE Phi = []
> sigmaRE Empty = []


Testing if a regular expression is empty (empty word)

> isEmpty :: RE a -> Bool
> isEmpty Phi = False
> isEmpty Empty = True
> isEmpty (Choice r1 r2) = (isEmpty r1) || (isEmpty r2)
> isEmpty (Seq r1 r2) = (isEmpty r1) && (isEmpty r2)
> isEmpty (Star r) = True
> isEmpty (L _) = False

Testing if a regular expression contains nothing

> isPhi :: RE a -> Bool
> isPhi Phi = True
> isPhi Empty = False
> isPhi (Choice r1 r2) = (isPhi r1) && (isPhi r2)
> isPhi (Seq r1 r2) = (isPhi r1) || (isPhi r2)
> isPhi (Star r) = False
> isPhi (L _) = False


Brzozowski's derivative operation
deriv r l denotes the regular expression where the
"leading l has been removed"
(not necessary for the intersection algorithm,
only included to illustrate the difference
to the upcoming partial derivative algorithm)

> deriv :: Eq a => RE a -> a -> RE a
> deriv Phi _ = Phi
> deriv Empty _ = Phi
> deriv (L l1) l2
> | l1 == l2 = Empty
> | otherwise = Phi
> deriv (Choice r1 r2) l =
> Choice (deriv r1 l) (deriv r2 l)
> deriv (Seq r1 r2) l =
> if isEmpty r1
> then Choice (Seq (deriv r1 l) r2) (deriv r2 l)
> else Seq (deriv r1 l) r2
> deriv (this@(Star r)) l =
> Seq (deriv r l) this



(a variant) of Antimirov's partial derivative operation

Antimirov demands that partDeriv (Star (L 'A')) 'A' yields [A*]
whereas our version yields [<<>,'A'*>].
The difference is not essential here.

> partDeriv :: Eq a => RE a -> a -> [RE a]
> partDeriv Phi l = []
> partDeriv Empty l = []
> partDeriv (L l') l
> | l == l' = [Empty]
> | otherwise = []
> partDeriv (Choice r1 r2) l = nub ((partDeriv r1 l) ++ (partDeriv r2 l))
> partDeriv (Seq r1 r2) l
> | isEmpty r1 =
> let s1 = [ (Seq r1' r2) | r1' <- partDeriv r1 l ]
> s2 = partDeriv r2 l
> in nub (s1 ++ s2)
> | otherwise = [ (Seq r1' r2) | r1' <- partDeriv r1 l ]
> partDeriv (Star r) l = [ (Seq r' (Star r)) | r' <- partDeriv r l ]


Here's finally the partial derivative based intersection algorithm.


> type Env a = [((RE a, RE a), RE a)]


> intersectRE :: Eq a => RE a -> RE a -> RE a
> intersectRE r1 r2 = intersectC [] r1 r2

> intersectC :: Eq a => Env a -> RE a -> RE a -> RE a
> intersectC env r1 r2
> | r1 == Phi || r2 == Phi = Phi
> | r1 == Empty || r2 == Empty = Empty
> | otherwise =
> case lookup (r1,r2) env of
> Just r -> r
> Nothing ->
> let letters = sigmaRE (r1 `Choice` r2)
> env' = ((r1,r2),r):env
> r1l l = resToRE $ partDeriv r1 l
> r2l l = resToRE $ partDeriv r2 l
> r' = resToRE $ map (\l -> Seq (L l) (intersectC env' (r1l l) (r2l l))) letters
> r = if (isEmpty r1) && (isEmpty r2)
> then Choice r' Empty
> else r'
> in r

The problem with the algorithm is that we use recursion in Haskell to model
recursive proofs. For example, try

intersect rAstar rAstar




Converting a regular equation into a regular expression

We assume that variables x appears (if at all) at position (r,Var x)
convert2 traveres the regexp and yields (r1,r2)
where the invariant is that r1 is part of the loop and r2 is the base case

> convert :: Int -> RE a -> RE a
> convert x r = let (r1,r2) = convert2 x r
> in Seq (Star r1) r2

> convert2 :: Int -> RE a -> (RE a, RE a)
> convert2 x Empty = (Empty, Empty)
> convert2 x (Var y)
> | x == y = (Empty,Empty)
> | otherwise = (Empty, Var y) -- can this happen?
> convert2 x (r@(Seq l r1))
> | contains x r1 = let (r2,r3) = convert2 x r1
> in (Seq l r2, r3)
> | otherwise = (Empty, r)
> convert2 x (Choice r1 r2) = let (r1', r1'') = convert2 x r1
> (r2', r2'') = convert2 x r2
> in (Choice r1' r2', Choice r1'' r2'')

> contains :: Int -> RE a -> Bool
> contains x (Var y) = x == y
> contains x (Seq r1 r2) = contains x r1 || contains x r2
> contains x (Star r) = contains x r
> contains x (Choice r1 r2) = contains x r1 || contains x r2
> contains x _ = False


We use first-order syntax to represent recursive proofs/regular expressions.
We then use convert to actually build the non-recursive regular expression.


> intersectRE2 :: Eq a => RE a -> RE a -> RE a
> intersectRE2 r1 r2 = intersectC2 1 [] r1 r2

> intersectC2 :: Eq a => Int -> Env a -> RE a -> RE a -> RE a
> intersectC2 cnt env r1 r2
> | r1 == Phi || r2 == Phi = Phi
> | r1 == Empty || r2 == Empty = Empty
> | otherwise =
> case lookup (r1,r2) env of
> Just r -> r
> Nothing ->
> let letters = sigmaRE (r1 `Choice` r2)
> env' = ((r1,r2),Var cnt):env
> r1l l = resToRE $ partDeriv r1 l
> r2l l = resToRE $ partDeriv r2 l
> r' = resToRE $ map (\l -> Seq (L l) (intersectC2 (cnt+1) env' (r1l l) (r2l l))) letters
> r = if (isEmpty r1) && (isEmpty r2)
> then Choice r' Empty
> else r'
> in convert cnt r


For testing purposes, it's handy to have a function which tests for (semantic)
equality among regular expressions (again written using partial derivatives).


> type EnvEq a = [(RE a, RE a)]

> eqRE :: Eq a => RE a -> RE a -> Bool
> eqRE r1 r2 = eqREC [] r1 r2

> eqREC :: Eq a => EnvEq a -> RE a -> RE a -> Bool
> eqREC env r1 r2
> | isEmpty r1 && (not (isEmpty r2)) = False
> | isPhi r1 && (not (isPhi r2)) = False
> | otherwise =
> if elem (r1,r2) env
> then True
> else let letters = sigmaRE (r1 `Choice` r2)
> env' = (r1,r2):env
> r1l l = resToRE $ partDeriv r1 l
> r2l l = resToRE $ partDeriv r2 l
> in and $ map (\l -> eqREC env' (r1l l) (r2l l)) letters

examples

> rA = L 'A'
> rAstar = Star rA
> rB = L 'B'
> rBstar = Star rB
> rAorBstar = Star (Choice rA rB)

Some sample runs (using intersectRE2, intersectRE won't terminate for interesting cases)

*RegExpIntersection> intersectRE2 rAstar rBstar
<((<>|<>)|<>)*,((<'A',{}>|<'B',{}>)|<>)>
*RegExpIntersection> eqRE Empty (intersectRE2 rAstar rBstar)
True
*RegExpIntersection> intersectRE2 rAorBstar rBstar
<((<>|<>)|<>)*,((<'A',{}>|<'B',<((<>|<'B',<>>)|<>)*,((<'A',{}>|<>)|<>)>>)|<>)>
*RegExpIntersection> eqRE rBstar (intersectRE2 rAorBstar rBstar)
True
*RegExpIntersection> intersectRE2 rAorBstar rAorBstar
<((<>|<>)|<>)*,((<'A',<((<'A',<>>|<'B',<>>)|<>)*,((<>|<>)|<>)>>|<'B',<((<'A',<>>|<'B',<>>)|<>)*,((<>|<>)|<>)>>)|<>)>
*RegExpIntersection> eqRE rAorBstar (intersectRE2 rAorBstar rAorBstar)
True
*RegExpIntersection> eqRE rAstar (intersectRE2 rAorBstar rAorBstar)
False
*RegExpIntersection> eqRE rBstar (intersectRE2 rAorBstar rAorBstar)
False


The regular expressions generated by the convert function are 'very verbose'.
There's space for lots of improvement.

Tuesday, 28 October 2008

Multi-set rewrite rules with guards and a parallel execution scheme

Latest news/updates




  • Sat Dec 6 18:34:20 CET 2008:

    • Parallel join pattern with guards and propagation extension built on top of multisetrewrite.
    • Check here here for more information.

  • Wed Nov 12 11:08:47 CET 2008:


    • New multisetrewrite-0.1.1 version uploaded to hackage
    • Includes more examples, a CHRSolver.hs and Join.hs abstraction
      built on top of multi-set rewrite
    • Some fun examples using these abstractions: GossipingGirls and BaggerProblem.




Brief description




We provide a library for multi-set rewrite rules with guards. Rewrite rules are executed concurrently as long as they operate on non-overlapping left-hand sides. We make use of highly-concurrent, non-blocking data structures based on CAS lists. Thus, we can parallelize concurrent rule executions on a multi-core architecture.

The library is similar in style to the below described actor library. The difference is that while actors run concurrently, their receive clauses (sort of multi-set rewrite rules) are only executed sequentially.

Download



The multisetrewrite library is implemented in Haskell and available
via

http://hackage.haskell.org

(look for the multisetrewrite library among the Concurrency packages)

Examples



The library comes with two examples (will hopefully increase over time).

Concurrent stack



The gist of the multi-set rewrite rules describing a concurrent stack (the actual example in Stack.hs is more verbose, after all it's 'only' a library and not
a new compiler).


[push x, pop y] .->. y := x

[push x, stack s] .->. stack (x:s)

[pop y, stack s] `when` (isNotEmptyStack s) .->. let (x:xs) = s
y := x
stack xs


push is synchronous whereas pop and stack are asynchronous. The above shows how to encode join-patterns via multisetrewrite. We are more expressive than join-patterns because we also support guards, non-linear (aka shared) variables (doesn't show up in the above).

CHR solver



On top of multisetrewrite we implement a CHR solver. See CHR.hs in the distribution.
To illustrate the expressive power, we implement the mergesort algorithm
via multi-set rewrite rules.


Here's the gist of the rules (as said above already, the actual implementation is more verbose).

Leq(x,a) \ Leq(x,b) when a < b <==> Leq(a,b)
Merge(n,a), Merge(n,b) when a < b <==> \Leq(a,b),\Merge(n+1,a)



Points to note:

  • The right-hand side of the first rule uses a mix of propagation and simplification. Leq(x,a) is propagated (ie not removed) whereas Leq(x,b) is simplified.
  • We make use of non-linear variables and guards in both rules.

Monday, 20 October 2008

Actors with Multi-Headed Receive Clauses

The actor model provides high-level concurrency abstractions to coordinate simultaneous computations by message passing. Languages implementing the actor model such as Erlang commonly only support single-headed pattern matching over received messages.
In

Martin Sulzmann, Edmund S. L. Lam, Peter Van Weert:
Actors with Multi-headed Message Receive Patterns.
COORDINATION 2008: 315-330

we propose an extension of the Actor model with receive clauses supporting multi-headed message patterns.

Here's a simple example of a market-place actor

receive
Seller x, Buyer x -> "match found"


We employ the combination of multiple messages in a receive pattern and non-linear patterns to test for a matching seller and a buyer. Non-linear patterns are in fact a short-hand for guards. That is, the above is equivalent to

receive
Seller x, Buyer y when x == y -> "match found"


The formal details of a such an enriched actor model are described in the above mentioned paper. We have also implemented the system as a library extension in Haskell. More on this below.



Haskell-Actor Implementation



Download



Available via

http://hackage.haskell.org

(look for the actor library among the Concurrency packages)

Overview



The Haskell-Actor implementation makes use of


  • Haskell channels to represent the actors mailbox, and
  • user-definable pattern matching implemented via type class overloading.


Haskell channels provide the basic abstraction to write (send) and read (receive) from a channel (mailbox). Thus, we can straightforwardly model actors with *single-headed* receive clauses. That is, we read messages one at a time and check for the occurrence of a specific message. The novelty of Haskell-Actor mailboxes is that we can test for the ocurrence of multiple messages via *multi-headed* receive clauses (see the above market-place example).

Messages are user-definable via Haskell data types. The user needs to provide some boiler-plate code (type class instances) to define message pattern matching.


Details



To use Haskell-Actor library you'll need
to understand the following combinators.


  • receive
  • send
  • createActor
  • runActor
  • kill


We'll discuss each of the above in turn.

receive



receive is similar to case statements in Haskell. One difference is that we can match against multiple messages (see the above market-place actor).

Haskell doesn't allow us to overload the pattern matching syntax (it's a library extension). We solve this by providing (generic) primitives to implement multi-headed message pattern matching in receive clauses by providing a (generic) set of primitives which need to be extended by the user for the specific message type (described as a data type).

For example, consider the following simple message type found in the Chain.hs example


data Msg = Blah deriving (Eq,Show)


There are two things, the user needs to provide.


  • Hash-map: Message are indexed based on their constructor names to speed up the search for matching message patterns.


    valhashOp = HashOp { numberOfTables = 1, hashMsg = \ _ -> 1 }


  • Specific pattern matcher:


    instance EMatch Msg where
    match tags m1 m2 = return (m1 == m2, tags)


    We extend the generic matcher by a message specific case.



By providing the hash-map and the message-specific matcher, we can define an actor which waits for the 'Blah' message to arrive and then sends the same message to its neighbor.


actorChain neighbor self =
receive self
[ [Blah] .->. send (toPID neighbor) Blah ]


NOTE: The receive statement is similar to case statements in Haskell. That is, we make explicit the actor/mailbox to which we apply a list of receive clauses. In Erlang, the actor/mailbox is implicit.

send



Given the pid (process identification number, similar to Erlang) we can send a message to an actor. For example,


send (toPID neighbor) Blah


toPID is a primitive which extracts the pid from the neighbor actor

createActor




createActor :: HashOp msg -> IO (Act msg)

creates a new actor for a specific message type, given
a hash-map. For example,

(initialActor :: Act Msg) <- createActor valhashOp


runActor




runActor :: Act msg -> (Act msg -> IO ()) -> IO ()


We spawn a new (Haskell) thread in which we apply the first argument (the actor) to the second argument (the behavior). For example,


runActor curr (actorChain prev)

where curr refers to the current actor and prev to the previous actor.


kill




kill :: PID msg -> IO ()


simply kills the thread (we don't kill any sub-actor threads, must be taken care of by the user).

Examples



The below examples are part of the distribution.

Chain.hs



Creates some n number of actors which pass around some message.


PingPong.hs



The standard ping-pong actor example. Simply call the main function and see what's happening.

MarketPlace.hs



A market-place using server and client actors. Call the main function to invoke the server. To invoke a client open a new terminal and execute 'telnet localhost 4242' for connecting clients to the server. You'll be asked for your name (sent to the server and the server informs everybody about new clients) and what item you'd like to sell or buy. The server then checks for matching buyers and sellers.

This example uses pattern variables and multi-headed pattern receive clauses.
Pattern variable need to be created explicitly because we implement actors
(i.e. pattern matching over messages) as a library.
Here are some code snippets.


; x <- newVar :: IO (VAR String)
; let go =
receive client
[ [arrivedMsg x] .->.
do { v1 <- readVar x
; hPutStrLn hdl ("\n Arrived: " ++ show v1)
; go
}
, ... ]


We explicitly create a pattern variable x which we then
use in the message pattern 'arrivedMsg x'.

To distinguish between values and variables we use 'lifted' types.


data L a = Val a
| Var (VAR a) deriving Eq
-- see ActorBase.hs for the internal variable representation
-- (only for the curious reader/user)

data MsgClient = Arrived (L String)
-- notifies about newly arrived clients


It's of course pretty clumsy to write down lifted types.
Here's a nicer (type class) interface.


-- client interface
class ArrivedMsg a where
arrivedMsg :: a -> MsgClient

instance ArrivedMsg (VAR String) where
arrivedMsg x = Arrived (Var x)
instance ArrivedMsg String where
arrivedMsg s = Arrived (Val s)



In case of many different types of messages/constructors, this 'boilerplate' code is straightforward but tedious to write down. We should eventually look into Template Haskell (future work).

Thursday, 1 May 2008

Partial Derivative Regular Expression Pattern Matching



Regular expression pattern matching as found in domain-specific
languages such as XDuce, CDuce, XHaskell is a highly useful
concept but is not commonly supported by mainstream languages.
Below I give an elementary Haskell implementation of regular expression
pattern matching based on (partial) derivatives of regular expressions.


This work is part of the XHaskell project, carried
out in collaboration with my PhD student Kenny Lu Zhuo.
Thanks to Burak Emir for helpful discussions
(and suggesting the name partial derivate regexp pattern matching).

This post is a literate Haskell file (converted to html thanks
to Malcolm Wallace's hscolour).

---------------
-- Motivation

Our goal is to understand and implement pattern matching involving
regular expressions a la XDuce, CDuce and XHaskell.
Here's a simple example that illustrates what's going on.

f :: (Space | Text)* -> Text*
f () = ()
f (x : Text+, y : (Space | Text)*) = (x, f y)
f (x : Space*, y : (Space | Text)*) = f y

The above function removes all (white) space from a text.
We assume that Text refers to some alpha-numeric character.

We expect that

f " Hello Bye" yields "HelloBye"

Here's what's happening during the evaluation of f " Hello Bye".

We match the input " Hello Bye" against each pattern clause
(from top to bottom)

The first clause cleary doesn't apply, so does not the second clause
becaues the pattern (x : Text+, y : (Space | Text)*) matches only
input that starts with some Text.
The third pattern (x : Space*, y : (Space | Text)*) applies.
The subpattern x : Space* binds any number of spaces. We assume
that we greedily consumes spaces. Hence, the pattern match
(x : Space*, y : (Space | Text)*) against " Hello Bye" yields "HelloBye"
yields

x holds " " (the three leading spaces)
y holds "Hello Bye" (the rest)

(Note: We view here a string as a concenation of Space and Text)

Having established the binding of pattern variables, we can
execute the body of the pattern clause. This leads to

f "Hello Bye"

Again, we check which pattern matches the input "Hello Bye".
This time the second pattern applies and we find that

x holds "Hello" (all non-empty text)
y holds " Bye" (the rest)

The subsequent call is

f " Bye"

It should be clear now how the rest of the computation progresses.
We keep all text but throw away all spaces.
Hence,

f " Hello Bye"

evaluates to

"HelloBye"


The main difference to pattern matching a la ML and Haskell is that
we can NOT perform the pattern match by comparing the structure
of the pattern against the structure of the incoming value.
The reason is that a pattern like

(x : A*)

can possibly match a number of structurally different values such as

"" (also known as epsilon)

"A"

"AA"

and so on


The challenge is that we need to take into account the semantic
meaning of regular expressions when performing the pattern match.

Here's another tricky example.
Matching the input "AB" against the pattern (x:A*, y:((A,B)* | B))
yields the following pattern bindings

(x,""), (y,"AB")

and

(x,"A"), (y,"B")

This shows that regular expression pattern matching
is indeterministic (unless we fix a specific pattern matching policy).


-----------------------------------------------
-- Formalizing the Pattern Matching Relation


We first need to fix the language of regular expressions and patterns.


r ::= r + r -- choice
-- later, we often write (r | r) instead of (r + r)
| (r,r) -- concatenation
| r* -- repetition
| epsilon -- empty word
| A | B | ... -- alphabet symbols/letters

p ::= (x : r) -- r is a regular expression
| (p,p) -- pairs
| (p + p) -- choice



The pattern matching relation

w <| p ~> env

pronounced

"word w matches pattern p and yiels the environment env"

(Note: words are strings, sequences of letters/characters)


Here are the rules describing all valid pattern matching relations.
We write L(r) to denote the language describe by a regular expression.


w in L(r)
(Var) -------------------------
w <| (x :: r) ~> [(x,w)]


w = w1 w2
w1 <| p1 ~> env1
w2 <| p2 ~> env2
(Pair) -----------------------------
w <| (p1,p2) ~> env1 ++ env2


w <| p1 ~> env1
(Choice1) ------------------------
w <| p1 + p2 ~> env1


w <| p2 ~> env2
(Choice1) ------------------------
w <| p1 + p2 ~> env2


How to implement w <| p ~> env
How to cope with indeterminism?

For example, consider

(1)

AA <| (x : A*, y : A*)

~> [(x,epsilon), (y,AA)]

~> [(x,A), (y,A)]

~> [(x,AA), (y,epsilon)]


A sample derivation for the first case


epsilon in L(A*)
----------------------------------
epsilon <| (x:A*) ~> [(x,epsilon)]


AA in L(A*)
-----------------------
AA <| (y:A*) ~> [(y,AA)]

------------------------------------------------
AA <| (x : A*, y : A*) ~> [(x,epsilon), (y,AA)]

(2)

Recall the earlier example.

AB <| (x: A*, y : ((A,B)* | B))

~> [(x,A), (y,B)]

~> [(x,epsilon), (y,AB)]


Before we develop an algorithm for the
regular expression pattern matching problem
let's consider a simpler problem:

How to check that w is in L(r), pronounced as

"Word w matches the regular expression r"

(This is also known as the word problem)

We solve the word problem by applying the derivative algorithm:

w matches r iff

case w = epsilon: isEmpty r

isEmpty yields True if the r is empty, otherwise False
The definition is straightforward. See below.

case w = (l,v): v matches r\l

where r\l is the derivative of r wrt l


We obtain r\l by take away all "leading" l's.
Semantically, we can explain the derivative
operation as follows:

L(r\l) = { w | lw in L(r) }

Below we define a function which computes an
expression r\l representing the derivative of
r wrt l.

We can build the derivative r\l by composition
of its partial derivatives.
For example,

(r1 | r2)\l = r1\l | r2\l

We call r1\l the partial derivative of (r1 | r2)\l.
Therefore, we often refer to derivatives as
partial derivatives.

Here's the implementation in Haskell.

The regular expression language, parameterized over some alphabet

> data RE a where
> Phi :: RE a -- empty language
> Empty :: RE a -- empty word
> L :: a -> RE a -- single letter taken from alphabet a
> Choice :: RE a -> RE a -> RE a -- r1 + r2
> Seq :: RE a -> RE a -> RE a -- (r1,r2)
> Star :: RE a -> RE a -- r*
> deriving Eq

Some combinators

> re_star r = Star r
> re_empty = Empty
> re_letter l = L l
> re_choice r1 r2 = Choice r1 r2
> re_pair r1 r2 = Seq r1 r2

A word is a list of alphabet letters

> type Word a = [a]

Pretty printing of regular expressions

> instance Show a => Show (RE a) where
> show Phi = "{}"
> show Empty = "<>"
> show (L c) = show c
> show (Choice r1 r2) = ("(" ++ show r1 ++ "|" ++ show r2 ++ ")")
> show (Seq r1 r2) = ("<" ++ show r1 ++ "," ++ show r2 ++ ">")
> show (Star r) = (show r ++ "*")


Matching words against regular expressions

> matchWord :: Eq a => RE a -> Word a -> Bool
> matchWord r [] = isEmpty r
> matchWord r (l:w) = matchWord (partDeriv r l) w

> isEmpty :: RE a -> Bool
> isEmpty Phi = False
> isEmpty Empty = True
> isEmpty (Choice r1 r2) = (isEmpty r1) || (isEmpty r2)
> isEmpty (Seq r1 r2) = (isEmpty r1) && (isEmpty r2)
> isEmpty (Star r) = True
> isEmpty (L _) = False

> partDeriv :: Eq a => RE a -> a -> RE a
> partDeriv Phi _ = Phi
> partDeriv Empty _ = Phi
> partDeriv (L l1) l2 = if l1 == l2 then Empty else Phi
> partDeriv (Choice r1 r2) l = Choice (partDeriv r1 l) (partDeriv r2 l)
> partDeriv (Seq r1 r2) l =
> if isEmpty r1
> then Choice (Seq (partDeriv r1 l) r2) (partDeriv r2 l)
> else Seq (partDeriv r1 l) r2
> partDeriv (this@(Star r)) l =
> Seq (partDeriv r l) this


Most of the cases are straightforward.
In case of (r1, r2) \ l we need to take care of the case that r1 is empty!

Here's an example

partDeriv (A|B)* A
= ( partDeriv (A|B) A , (A|B)* )
= ( (partDeriv A A) | (partDeriv B A), (A|B)*)
= ( () | Phi, (A|B)*)

effectively

= (A|B)*

The above also explains why we need Phi.


some examples

> r1 = (Choice (Star (Seq (L 'A') (L 'B'))) (L 'B')) -- ((A,B)*|B)
> r2 = Seq (Star (L 'A')) (Star (L 'A')) -- (A*,A*)
> r3 = Star (Choice (L 'A') (L 'B')) -- (A|B)*

> w1 = "AABBAAA"
> m1 = matchWord r1 w1
> m2 = matchWord r2 w1
> m3 = matchWord r3 w1


Let's get back to our problem of implementing
the pattern matching relation

w <| p ~> env


--------------------------------------------------
-- Towards a regexp pattern matching algorithm


The key idea: We apply the idea of derivatives to pattern matching


(l,w) <| p ~> env iff w <| pdPat p l ~> env

(l,w) matches the pattern p and yields environment Env
iff w matches the (partial) pattern derivative p wrt l

How is pdPat defined?

The easy case first.

pdPat (p1 | p2) l = (pdPat p1 l) | (pdPat p2 l)

What about

pdPat (x:r) l = ?

We can't simply replace ? by (x: r\l).
Here building the derivative r\r of r wrt l means that
we have consumed the input symbol l. But we must
record somewhere that we have consumed l.

The easiest method is to record with each
variable pattern the sequence of symbols
which have been consumed so far by that variable pattern.

So,

the variable pattern

<w> x : r

says that we have consumed so far w, hence,
any valid pattern binding will look like (x,w...),
but we yet need to consume any word v which
is accepted by r (ie v in L(r)).

The derivative definition for variable patterns
is then straightforward.

pdPat l (<w> x : r) = <w,l> x : r\l

Here's an example.

AB |> (x : (A|B)*) ~> env

Of course env = [(x,AB)]

In some intermediate steps we find

pdPat (<> x : (A|B)*) A = <A> x : (A|B)*
-- shortcut see earlier calculation
-- and *remember* that we consumed A

pdPat (<A> x : (A|B)*) B = <AB> x : (A|B)*


What about pair patterns?


pdPat (p1,p2) l = if isEmpty (strip p1)
then (pdPat p1 l, p2) | (??, pdPat p2 l)
else (pdPat p1 l, p2)

stip simply extracts the regular expression.
The question is what to replace ?? with ?

If p1 is empty this means that all further matching will helping in p2.
But we simply can't throw away p1 because we record the variable
binding in the pattern itself.
We also can't simply keep p1, we must indicate that the matching
uing p1 is finished.

The idea is to replace ?? by the pattern where we
make all regular expresssions empty (if possibly).

For example, consider the pattern

(<AB> x : (A|B)*, <> y : C*)

where x : (A|B)* has already consumed AB

and C is the remaining input.

We expect

pdPat (<AB> x : (A|B)*, <> y : C*) C
= (<ABC> x : Phi, <y> y : C*) | (<AB> x : (), <C> y : C*)

(A|B)* \ C = Phi

which shows that from (<ABC> x : Phi, <y> y : C*)
we can't obtain any valid pattern binding.

But (A|B)* is empty. Hence, we can stop matching
using the subpattern <AB> x : (A|B)* which we indicate
by replacing (A|B)* with () (the empty sequence).

In general, to stop matching uinsg p1 we need to make
the pattern p1 empty by replacing all regular expressions
which contain () by () and all others we replace by Phi.

Here's the implementation of pattern derivatives in Haskell.

The pattern language, we assume that patterns are linear


> data Pat a where
> PVar :: Int -> Word a -> RE a-> Pat a
> PPair :: Pat a -> Pat a -> Pat a
> PChoice :: Pat a -> Pat a -> Pat a

-- PVar var w r
-- variables var are represented by Ints
-- w represents the part we have already seen
-- r represents the remaining part we yet have to match


Combinators

> pat_var n r = PVar n [] r
> pat_pair p1 p2 = PPair p1 p2
> pat_choice p1 p2 = PChoice p1 p2

pretty printing

> instance Show a => Show (Pat a) where
> show (PVar i w r) = ("x"++show i ++ "::" ++ show r)
> show (PPair p1 p2) = ("<" ++ show p1 ++ "," ++ show p2 ++ ">")
> show (PChoice p1 p2) = "(" ++ show p1 ++ "|" ++ show p2 ++ ")"


(partial) derivative of patterns

> pdPat :: Eq a => Pat a -> a -> Pat a
> pdPat (PVar x w r) l = PVar x (w ++ [l]) (partDeriv r l)
> pdPat (PPair p1 p2) l =
> if (isEmpty (strip p1))
> then PChoice (PPair (pdPat p1 l) p2) (PPair (mkEmpPat p1) (pdPat p2 l))
> else PPair (pdPat p1 l) p2
> pdPat (PChoice p1 p2) l =
> PChoice (pdPat p1 l) (pdPat p2 l)

> strip :: Pat a -> RE a
> strip (PVar _ w r) = r
> strip (PPair p1 p2) = Seq (strip p1) (strip p2)
> strip (PChoice p1 p2) = Choice (strip p1) (strip p2)

replace all (<w> x : r) by (<w> x: <>) if isEmpty r
otherwise yield (<w> x: Phi)

> mkEmpPat :: Pat a -> Pat a
> mkEmpPat (PVar x w r)
> | isEmpty r = PVar x w Empty
> | otherwise = PVar x w Phi
> mkEmpPat (PPair p1 p2) = PPair (mkEmpPat p1) (mkEmpPat p2)
> mkEmpPat (PChoice p1 p2) = PChoice (mkEmpPat p1) (mkEmpPat p2)

An example to see the derivation operation on patterns in action

(<> x : A*, <> y : A*) and input AA

-->A (<A> x : A*, <> y : A*) | (<> x : (), <A> y : A*)

-->A
|
(<AA> x : A*, <> y : A*) | (<A> x : Phi, <A> y : A*)
| (<A> x : (), <A> y : A*) | | (<> x : (), <AA> y : A*)


Observation: We not only calculate one possible matching,
we calculate all matchings!

(No performance penalty thanks to lazy evaluation)


The binding of pattern variables to words

> type Env a = [(Int,Word a)]

> patMatch :: Eq a => Pat a -> Word a -> [Env a]
> patMatch p (l:w) =
> patMatch (pdPat p l) w
> patMatch (PVar x w r) [] =
> if isEmpty r then [[(x,w)]] else []
> patMatch (PChoice p1 p2) [] =
> (patMatch p1 []) ++ (patMatch p2 [])
> -- indet choice
> patMatch (PPair p1 p2) [] =
> (patMatch p1 []) `combine` (patMatch p2 [])
> -- build all possible combinations
> where
> combine xss yss = [ xs ++ ys | xs <- xss, ys <- yss]

> longPatMatch :: Eq a => Pat a -> Word a -> Maybe (Env a)
> longPatMatch p w =
> first (patMatch p w)
> where
> first (env:_) = return env
> first _ = Nothing


> shortPatMatch :: Eq a => Pat a -> Word a -> Maybe (Env a)
> shortPatMatch p w =
> last (patMatch p w)
> where
> last [env] = return env
> last (_:xs) = last xs
> last _ = Nothing