Proving Correctness of Translation from Moded Flat GHC to π-Calculus
Keiji Hirata · The MIT Press eBooks · 1995
This poster presents a translation from moded Flat Guarded Horn Clauses (FGHC) [4] to polyadic π-calculus (PPC) [3] and proves the correctness of the translation. This presentation introduces FGHC– (a subset of moded FGHC), presents the rules for translation from an FGHC– program to PPC statements, introduces the moded ground equality theory (MGE) in order to define the unification in FGHC–, and shows that the translation is correct with respect to the Ueda's operational semantics of GHC based on a transition system. FGHC– has almost the same descriptive power as FGHC and makes the translation quite straightforward [1]. Since every unification is directed (i.e. moded), each occurrence of FGHC– terms can be statically classified into either a generator or consumer of data. Correspondingly, the translator provides two kinds of PPC agents. A moded logical variable is basically translated into a PPC agent for duplication. Moreover, predicate invocation and the head of a definition clause are also represented by the same kinds of PPC agents. The data generation, consumption and duplication by PPC agents implement moded passive and active unification in FGHC–; MCE prescribes the unification in FGHC–. Then the transition rules of translated PPC statements for concurrent rewriting, one-step reduction, and active unification are given. Finally, these transition rules are proved to be equivalent to Ueda's operational semantics under MGE. Understanding FGHC– at the PPC level has the following advantages. This translation provides a new theoretical basis for investigating an interesting property, duality, where processes and messages of GHC play the same roles as data carriers [2]. Since translated PPC statements can be regarded as the specification of source pro grams in FGHC–, even the behavior of programs including nonlogical built-in predicates can be studied at the PPC level. Moreover, MGE gives us a new insight into well-moding and the groundness of moded variables.