\pi-Calculus Semantics of Moded Flat GHC

Keiji Hirata

Abstract:

This paper presents a new operational semantics for
moded Flat Guarded Horn Clauses (FGHC).
\pi-calculus is a simple model of concurrent computation based
upon the notion of naming; \pi-calculus agents concurrently exchange
names as data via names as channels.
Naming enables an agent to be encapsulated as a value and
also can provide the execution view that
independent states interact with one another.
The semantics of \pi-calculus has been investigated intensively
mainly from the algebraic point of view.
Given an FGHC program, we can consider that
the translated \pi-calculus statements represent
the operational meaning of the source program.
Such a \pi-calculus semantics has the following advantages:
both processes and messages (terms) are represented in a uniform way,
the semantics can specify nonlogical built-in predicates
together with ordinary predicates and logical variables, and
the various properties of \pi-calculus are well-understood theoretically.
This paper introduces FGHC- (a subset of moded FGHC),
presents the rules for translation from an FGHC- program to
polyadic \pi-calculus statements,
introduces the moded ground equality theory
in order to define the unification in FGHC-, and
shows that the new semantics is correct
with respect to the Ueda's conventional operational semantics of GHC
based on a transition system.