More Web Proxy on the site http://driver.im/

research-article

Memoryful geometry of interaction: from coalgebraic components to algebraic effects

Authors:

Naohiko Hoshino,

Ichiro HasuoAuthors Info & Claims

CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Article No.: 52, Pages 1 - 10

https://doi.org/10.1145/2603088.2603124

Published: 14 July 2014 Publication History

Abstract

Girard's Geometry of Interaction (GoI) is interaction based semantics of linear logic proofs and, via suitable translations, of functional programs in general. Its mathematical cleanness identifies essential structures in computation; moreover its use as a compilation technique from programs to state machines---"GoI implementation," so to speak---has been worked out by Mackie, Ghica and others. In this paper, we develop Abramsky's idea of resumption based GoI systematically into a generic framework that accounts for computational effects (nondeterminism, probability, exception, global states, interactive I/O, etc.). The framework is categorical: Plotkin & Power's algebraic operations provide an interface to computational effects; the framework is built on the categorical axiomatization of GoI by Abramsky, Haghverdi and Scott; and, by use of the coalgebraic formalization of component calculus, we describe explicit construction of state machines as interpretations of functional programs. The resulting interpretation is shown to be sound with respect to equations between algebraic operations, as well as to Moggi's equations for the computational lambda calculus. We illustrate the construction by concrete examples.

References

[1]

S. Abramsky. Retracing some paths in process algebra. In CONCUR '96: Concurrency Theory, volume 1119 of LNCS, pages 1--17. Springer Berlin Heidelberg, 1996.

Digital Library

[2]

S. Abramsky, E. Haghverdi, and P. Scott. Geometry of interaction and linear combinatory algebras. Math. Struct. in Comp. Sci., 12:625--665, 2002.

Digital Library

[3]

L. Aceto, W. Fokkink, and C. Verhoef. Structural operational semantics. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, pages 197--292. Elsevier, 2001.

[4]

C. Baier, M. Sirjani, F. Arbab, and J. J. M. M. Rutten. Modeling component connectors in Reo by constraint automata. Science of Computer Programming, 61(2):75--113, 2006.

Digital Library

[5]

L. S. Barbosa. Towards a calculus of state-based software components. Journal of Universal Computer Science, 9(8):891--909, 2003.

[6]

U. Dal Lago and U. Schöpp. Functional programming in sublinear space. In Programming Languages and Systems, volume 6012 of LNCS, pages 205--225. Springer Berlin Heidelberg, 2010.

Digital Library

[7]

V. Danos and L. Regnier. Reversible, irreversible and optimal λ-machines: Extended abstract. ENTCS, 3(0):40--60, 1996.

[8]

O. Fredriksson and D. R. Ghica. Seamless distributed computing from the geometry of interaction. In C. Palamidessi and M. D. Ryan, editors, Trustworthy Global Computing, volume 8191 of Lecture Notes in Computer Science, pages 34--48. Springer Berlin Heidelberg, 2013.

[9]

D. R. Ghica. Geometry of synthesis: a structured approach to VLSI design. In M. Hofmann and M. Felleisen, editors, POPL, pages 363--375. ACM, 2007. ISBN 1-59593-575-4.

Digital Library

[10]

J.-Y. Girard. Geometry of interaction 1: Interpretation of system F. In S. V. R. Ferro, C. Bonotto and A. Zanardo, editors, Logic Colloquium '88 Proceedings of the Colloquium held in Padova, volume 127 of Studies in Logic and the Foundations of Mathematics, pages 221--260. Elsevier, 1989.

[11]

G. Gonthier, M. Abadi, and J.-J. Lévy. The geometry of optimal lambda reduction. In R. Sethi, editor, POPL, pages 15--26. ACM Press, 1992. ISBN 0-89791-453-8.

Digital Library

[12]

M. Hasegawa. The uniformity principle on traced monoidal categories. ENTCS, 69(0):137--155, 2003. CTCS'02.

[13]

M. Hasegawa. On traced monoidal closed categories. Math. Struct. in Comp. Sci., 19:217--244, 4 2009. ISSN 1469-8072.

Digital Library

[14]

I. Hasuo and N. Hoshino. Semantics of higher-order quantum computation via geometry of interaction. In LICS, pages 237--246, 2011.

Digital Library

[15]

I. Hasuo and B. Jacobs. Traces for coalgebraic components. Mathematical Structures in Computer Science, 21:267--320, 4 2011.

Digital Library

[16]

N. Hoshino. A modified GoI interpretation for a linear functional programming language and its adequacy. In M. Hofmann, editor, FOSSACS, volume 6604 of Lecture Notes in Computer Science, pages 320--334. Springer, 2011.

Digital Library

[17]

B. Jacobs. From coalgebraic to monoidal traces. ENTCS, 264(2):125--140, 2010.

Digital Library

[18]

B. Jacobs. Introduction to coalgebra. towards mathematics of states and observations, Version 2.0 2012.

[19]

B. Jacobs, editor. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the Foundations of Mathematics. Elsevier, 19999.

[20]

A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119: 447--468, 4 1996.

[21]

B. Klin. Bialgebraic methods and modal logic in structural operational semantics. Information and Computation, 207(2):237--257, 2009.

Digital Library

[22]

Y. Lafont. Interaction combinators. Information and Computation, 137(1):69--101, 1997.

Digital Library

[23]

O. Laurent. A token machine for full geometry of interaction. In TLCA, pages 283--297, 2001.

Digital Library

[24]

J. Longley. Realizability Toposes and Language Semantics. PhD thesis, University of Edinburgh, 1994.

[25]

I. Mackie. The geometry of interaction machine. In R. K. Cytron and P. Lee, editors, POPL, pages 198--208. ACM Press, 1995. ISBN 0-89791-692-1.

Digital Library

[26]

E. Moggi. Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-66, Laboratory for Foundations of Computer Science, 1988.

[27]

K. Muroya, T. Kataoka, I. Hasuo, and N. Hoshino. Compiling effectful terms to transducers: Prototype implementation of memoryful geometry of interaction. Submitted, 2014.

[28]

G. Plotkin and J. Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69--94, 2003.

[29]

J. Power and E. Robinson. Premonoidal categories and notions of computation. Mathematical Structures in Computer Science, 7:453--468, 10 1997.

Digital Library

[30]

U. Schöpp. On interaction, continuations and defunctionalization. In TLCA, volume 7941 of LNCS, pages 205--220. Springer Berlin Heidelberg, 2013.

[31]

A. Simpson. Reduction in a linear lambda-calculus with applications to operational semantics. In G. Jürgen, editor, RTA, volume 3467 of LNCS, pages 219--234. Springer Berlin Heidelberg, 2005.

Digital Library

[32]

D. Turi and G. Plotkin. Towards a mathematical operational semantics. In LICS, pages 280--291. IEEE Computer Society, 1997.

Digital Library

[33]

A. Yoshimizu, I. Hasuo, C. Faggian, and U. Dal Lago. Measurements in proof nets as higher-order quantum circuits. In ESOP, 2014. To appear.

Digital Library

Cited By

Román M(2023)Promonads and String Diagrams for Effectful CategoriesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.380.20380(344-361)Online publication date: 7-Aug-2023
https://doi.org/10.4204/EPTCS.380.20
Castellan SClairambault P(2023)The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal UnfoldingProceedings of the ACM on Programming Languages10.1145/35712177:POPL(689-717)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571217
Di Lavore EGianola ARomán MSabadini NSobociński P(2023)Span(Graph): a canonical feedback algebra of open transition systemsSoftware and Systems Modeling10.1007/s10270-023-01092-722:2(495-520)Online publication date: 21-Mar-2023
https://doi.org/10.1007/s10270-023-01092-7
Show More Cited By

Index Terms

Memoryful geometry of interaction: from coalgebraic components to algebraic effects
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Formal languages and automata theory
    1. Formalisms
      1. Algebraic language theory
  2. Semantics and reasoning
    1. Program semantics
      1. Algebraic semantics

Recommendations

Memoryful geometry of Interaction II: recursion and adequacy
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

A general framework of Memoryful Geometry of Interaction (mGoI) is introduced recently by the authors. It provides a sound translation of lambda-terms (on the high-level) to their realizations by stream transducers (on the low-level), where the ...
Memoryful geometry of Interaction II: recursion and adequacy
POPL '16

A general framework of Memoryful Geometry of Interaction (mGoI) is introduced recently by the authors. It provides a sound translation of lambda-terms (on the high-level) to their realizations by stream transducers (on the low-level), where the ...
Musings around the geometry of interaction, and coherence

We introduce the Danos R gnier category DR(M) of a linear inverse monoid M, as a categorical description of geometries of interaction (GOI) inspired from the weight algebra. The natural setting for GOI is that of a so-called weakly Cantorian linear ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

July 2014

764 pages

ISBN:9781450328869

DOI:10.1145/2603088

Program Chairs:
Thomas Henzinger
Institute of Science and Technology (IST), Austria
,
Dale Miller
INRIA and LIX/Ecole Polytechnique, Palaiseau

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 July 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Japan Society for the Promotion of Science

Conference

CSL-LICS '14

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

CSL-LICS '14: JOINT MEETING OF the Twenty-Third EACSL Annual Conference on COMPUTER SCIENCE LOGIC

July 14 - 18, 2014

Vienna, Austria

Acceptance Rates

CSL-LICS '14 Paper Acceptance Rate 74 of 212 submissions, 35%;

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
191
Total Downloads

Downloads (Last 12 months)15
Downloads (Last 6 weeks)4

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Román M(2023)Promonads and String Diagrams for Effectful CategoriesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.380.20380(344-361)Online publication date: 7-Aug-2023
https://doi.org/10.4204/EPTCS.380.20
Castellan SClairambault P(2023)The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal UnfoldingProceedings of the ACM on Programming Languages10.1145/35712177:POPL(689-717)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571217
Di Lavore EGianola ARomán MSabadini NSobociński P(2023)Span(Graph): a canonical feedback algebra of open transition systemsSoftware and Systems Modeling10.1007/s10270-023-01092-722:2(495-520)Online publication date: 21-Mar-2023
https://doi.org/10.1007/s10270-023-01092-7
Di Lavore Ede Felice GRomán M(2022)Monoidal Streams for Dataflow ProgrammingProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533365(1-14)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533365
Ghica D(2021)Operational Semantics with Hierarchical Abstract Syntax GraphsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.334.1334(1-10)Online publication date: 8-Feb-2021
https://doi.org/10.4204/EPTCS.334.1
Accattoli BDal Lago UVanoni G(2021)The (In)Efficiency of interactionProceedings of the ACM on Programming Languages10.1145/34343325:POPL(1-33)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434332
Kuperberg DPinault LPous D(2021)Cyclic proofs, system t, and the power of contractionProceedings of the ACM on Programming Languages10.1145/34342825:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434282
Dal Lago UHoshino N(2021)The geometry of Bayesian programmingMathematical Structures in Computer Science10.1017/S096012952100039631:6(633-681)Online publication date: 7-Dec-2021
https://doi.org/10.1017/S0960129521000396
Di Lavore EGianola ARomán MSabadini NSobociński P(2021)A Canonical Algebra of Open Transition SystemsFormal Aspects of Component Software10.1007/978-3-030-90636-8_4(63-81)Online publication date: 28-Oct-2021
https://doi.org/10.1007/978-3-030-90636-8_4
Sprunger DKatsumata SBouyer P(2019)Differentiable causal computations via delayed traceProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470168(1-12)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470168
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents