Loading...
Please wait, while we are loading the content...
Similar Documents
Memoryful GoI with Recursion
| Content Provider | Semantic Scholar |
|---|---|
| Author | Muroya, Koko Hasuo, Ichiro |
| Copyright Year | 2015 |
| Abstract | In this preliminary report we extend our framework of memoryful Geometry of Interaction (mGoI) [Hoshino, Muroya & Hasuo, CSL-LICS 2014] by recursion. The mGoI framework provides a sound translation from λ-terms to transducers; notably it accommodates algebraic effects introduced by Plotkin and Power; and the translation, defined in terms of a coalgebraic component calculus, is extracted from categorical semantics (hence correct-byconstruction). In our current extension, recursion is additionally accommodated by introducing a new “fixed point” operator in the component calculus. I. GOI INTERPRETATION Girard’s Geometry of Interaction (GoI) [1] is originally introduced as semantics of linear logic proofs and, via the Curry-Howard correspondence (and the Girard transformation), it has been successfully applied to denotational semantics of higher-order functional programs. The resulting semantics give so-called “GoI interpretation” of programs; one of its notable features is that GoI interpretation of function application is given by interactions of a function and its arguments. Many representations of GoI interpretation have been studied so far: the original one by elements of a C∗-algebra (or a dynamic algebra) that can be seen as “valid paths” on type derivation trees [1]; the one by token machines [2]; and the categorical one by arrows in a traced symmetric monoidal category [3]. The second one by token machines plays an important role in bridging the gap between mathematical interpretation and low-level implementation. Namely it provides techniques of compilation and high-level synthesis, such as a compilation technique [2] and a high-level synthesis technique [4] that enables hardware acceleration of programs by FPGA. We wish to contribute to this sequence of work by enable GoI interpretation to accommodate computational effects. II. MEMORYFUL GOI In the previous work [5] we developed the memoryful GoI (mGoI) framework that extends GoI interpretation of programs. Notably it accommodates algebraic effects—computational effects with algebraic operations as a syntactic interface, introduced by Plotkin and Power [6], [7]. Their examples include: nondeterminism, with a nondeterministic choice operation t as an algebraic operation; probability, with a probabilistic choice operation tp for any p ∈ [0, 1]; and global states, with operations lookup and update. A. Component Calculus over Transducers The mGoI interpretation of a program is given by T transducers—an extension of Mealy machines (or sequential machines) by effects specified by a monad T . Here we follow [8] and model algebraic effects by a monad T on the category Set of sets and functions. Definition II.1 (T -transducers [5, Definition 4.1]). For sets A and B, a T -transducer (X, c, x) from A to B (written as (X, c, x) : A _ B) consists of a set X , a function c : X×A→ T (X ×B) and an element x ∈ X . |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://lola15.tcs.ifi.lmu.de/muroya_hoshino_hasuo.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
