Geometry of interaction

Last updated

In proof theory, the Geometry of Interaction (GoI) was introduced by Jean-Yves Girard shortly after his work on linear logic. In linear logic, proofs can be seen as various kinds of networks as opposed to the flat tree structures of sequent calculus. To distinguish the real proof nets from all the possible networks, Girard devised a criterion involving trips in the network. Trips can in fact be seen as some kind of operator [ clarification needed ] acting on the proof. Drawing from this observation, Girard [1] described directly this operator from the proof and has given a formula, the so-called execution formula, encoding the process of cut elimination at the level of operators. Subsequent constructions by Girard proposed variants in which proofs are represented as flows [2] , or operators in von Neumann algebras [3] . Those models were later generalised by Seiller's Interaction Graphs models [4] .

One of the first significant applications of GoI was a better analysis [5] of Lamping's algorithm [6] for optimal reduction for the lambda calculus. GoI had a strong influence on game semantics for linear logic and PCF.

Beyond the dynamic interpretation of proofs, geometry of interaction constructions provide models of linear logic, or fragments thereof. This aspect has been extensively studied by Seiller [7] under the name of linear realisability, a version of realizability accounting for linearity.

GoI has been applied to deep compiler optimisation for lambda calculi. [8] A bounded version of GoI dubbed the Geometry of Synthesis has been used to compile higher-order programming languages directly into static circuits. [9]

Related Research Articles

In programming language theory, lazy evaluation, or call-by-need, is an evaluation strategy which delays the evaluation of an expression until its value is needed and which also avoids repeated evaluations.

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.

Linear logic is a substructural logic proposed by French logician Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics, as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction.

In functional programming, continuation-passing style (CPS) is a style of programming in which control is passed explicitly in the form of a continuation. This is contrasted with direct style, which is the usual style of programming. Gerald Jay Sussman and Guy L. Steele, Jr. coined the phrase in AI Memo 349 (1975), which sets out the first version of the Scheme programming language. John C. Reynolds gives a detailed account of the numerous discoveries of continuations.

Bunched logic is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics, which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic, and in systems modelling, where it provides a way to decompose the resources used by components of a system.

In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, F*, Epigram, Idris, and Lean, dependent types help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.

In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation.

<span class="mw-page-title-main">John C. Reynolds</span> American computer scientist (1935–2013)

John Charles Reynolds was an American computer scientist.

<span class="mw-page-title-main">Programming language theory</span> Branch of computer science

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.

In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion language of separation logic is a special case of the logic of bunched implications (BI). A CACM review article by O'Hearn charts developments in the subject to early 2019.

In theoretical computer science, the modal μ-calculus is an extension of propositional modal logic by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic.

The annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) is an academic conference in the field of computer science, with focus on fundamental principles in the design, definition, analysis, and implementation of programming languages, programming systems, and programming interfaces. The venue is jointly sponsored by two Special Interest Groups of the Association for Computing Machinery: SIGPLAN and SIGACT.

Interaction nets are a graphical model of computation devised by French mathematician Yves Lafont in 1990 as a generalisation of the proof structures of linear logic. An interaction net system is specified by a set of agent types and a set of interaction rules. Interaction nets are an inherently distributed model of computation in the sense that computations can take place simultaneously in many parts of an interaction net, and no synchronisation is needed. The latter is guaranteed by the strong confluence property of reduction in this model of computation. Thus interaction nets provide a natural language for massive parallelism. Interaction nets are at the heart of many implementations of the lambda calculus, such as efficient closed reduction and optimal, in Lévy's sense, Lambdascope.

In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way that knowledge of the realizer gives knowledge about the truth of the formula. There are many variations of realizability; exactly which class of formulas is studied and which objects are realizers differ from one variation to another.

In type theory, an empty type or absurd type, typically denoted is a type with no terms. Such a type may be defined as the nullary coproduct. It may also be defined as the polymorphic type

In computer science, polymorphic recursion refers to a recursive parametrically polymorphic function where the type parameter changes with each recursive invocation made, instead of staying constant. Type inference for polymorphic recursion is equivalent to semi-unification and therefore undecidable and requires the use of a semi-algorithm or programmer-supplied type annotations.

In computer science, region-based memory management is a type of memory management in which each allocated object is assigned to a region. A region, also called a zone, arena, area, or memory context, is a collection of allocated objects that can be efficiently reallocated or deallocated all at once. Memory allocators using region-based managements are often called area allocators, and when they work by only "bumping" a single pointer, as bump allocators.

<span class="mw-page-title-main">F* (programming language)</span> Functional programming language inspired by ML and aimed at program verification

F* is a high-level, multi-paradigm, functional and object-oriented programming language inspired by the languages ML, Caml, and OCaml, and intended for program verification. It is a joint project of Microsoft Research, and the French Institute for Research in Computer Science and Automation (Inria). Its type system includes dependent types, monadic effects, and refinement types. This allows expressing precise specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of satisfiability modulo theories (SMT) solving and manual proofs. For execution, programs written in F* can be translated to OCaml, F#, C, WebAssembly, or assembly language. Prior F* versions could also be translated to JavaScript.

In rewriting, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an evaluation strategy.

References

  1. ↑ Girard, Jean-Yves (1989). "Geometry of interaction 1: Interpretation of System F". Studies in Logic and the Foundations of Mathematics. 127: 221–260.
  2. ↑ Girard, Jean-Yves (1995). "Geometry of Interaction III: accomodating the additives". London Mathematical Society Lecture Notes Series: 329–389.
  3. ↑ Girard, Jean-Yves (2011). "Geometry of interaction V: logic in the hyperfinite factor". Theoretical Computer Science. 412 (20): 1860–1883.
  4. ↑ Seiller, Thomas (2016). "Interaction graphs: Full linear logic". Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science.
  5. ↑ Gonthier, G.; Abadi, M. N.; Lévy, J. J. (1992). "The geometry of optimal lambda reduction". Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '92. p. 15. doi:10.1145/143165.143172. ISBN   0897914538. S2CID   7265545.
  6. ↑ Lamping, J. (1990). "An algorithm for optimal lambda calculus reduction". Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90. pp. 16–30. doi:10.1145/96709.96711. ISBN   0897913434. S2CID   16333787.
  7. ↑ Seiller, Thomas (2024). Mathematical Informatics (Habilitation thesis). Université Sorbonne Paris Nord.
  8. ↑ Mackie, I. (1995). "The geometry of interaction machine". Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '95. pp. 198–208. doi:10.1145/199448.199483. ISBN   0897916921. S2CID   19000897.
  9. ↑ Dan R. Ghica. Function Interface Models for Hardware Compilation. MEMOCODE 2011.

Further reading

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.