\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.