权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Effects and algebraic theories.

效应和代数理论。

基本信息

批准号：
2054731
负责人：
金额：
--
依托单位：
University of Oxford
依托单位国家：
英国
项目类别：
Studentship
财政年份：
2018
资助国家：
英国
起止时间：
2018 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=studentship-2054731
关键词：
Effects algebraic theories.

项目摘要

This project falls within the EPSRC Information and communication technologies (ICT) research theme.This project is concerned with the foundations of programming languages, their semantics and type systems. Computational effects are a feature of programming languages representing impure behaviour, such as input and output operations, exceptions, state, nondeterminism. These operations are widely used in practical programming and are provided by many programming languages. However, their mathematical foundations have not been fully explored yet.In his influential work, Moggi gives a general denotational semantics for computational effects using monads. His idea was subsequently implemented in the pure functional language by Haskell, where monads are used to simulate side effects. Plotkin and Power introduce the idea of algebraic effects, a particular approach to computational effects where the impure behaviour results from a set of operations. The properties of these operations are specified by equations, making it possible to present algebraic effects as algebraic theories, traditionally studied in universal algebra. Each algebraic theory gives rise to a monad, thus exhibiting the connection with Moggi's semantics.In order to interpret effects, various extensions of first-order algebraic theories have been proposed. Examples include parameterised algebraic theories, proposed by Staton, and second-order algebraic theories developed by Fiore, Hur and Mahmoud. Fiore and Staton use substitution algebras and right lambda algebras, particular instances of second-order algebraic theories, to model jump effects and computation involving stacks of code pointers, respectively.Exploring further the connection between effects and second-order algebraic theories is a promising research direction that I will pursue. The goal is to find other algebraic theories that give rise to effects and vice-versa. In the first instance, this approach will lead to a better understanding of the semantics of effects. In the long term, the connection between effects and algebra could provide a general framework for extending programming calculi with computational effects. These extensions could then be implemented on top of high-level general-purpose programming languages. Within the ICT research theme, this project is part of the Theoretical Computer Science area because it employs formal reasoning, logical concepts and semantics. The project is also part of the Programming languages and compilers area since its aim is to understand programming languages better, and may lead to new implementations.

该项目属于 EPSRC 信息和通信技术 (ICT) 研究主题。该项目涉及编程语言的基础、语义和类型系统。计算效应是代表不纯行为的编程语言的一个特征，例如输入和输出操作、异常、状态、非确定性。这些操作在实际编程中被广泛使用，并且由许多编程语言提供。然而，它们的数学基础尚未得到充分探索。 Moggi 在他有影响力的著作中给出了使用单子的计算效果的一般指称语义。他的想法随后被 Haskell 用纯函数式语言实现，其中使用 monad 来模拟副作用。 Plotkin 和 Power 引入了代数效应的概念，这是一种计算效应的特殊方法，其中不纯行为是由一组运算产生的。这些运算的性质由方程指定，使得将代数效应呈现为代数理论成为可能，传统上在普适代数中研究。每个代数理论都会产生一个单子，从而表现出与莫吉语义的联系。为了解释效果，人们提出了一阶代数理论的各种扩展。例子包括 Staton 提出的参数化代数理论，以及 Fiore、Hur 和 Mahmoud 提出的二阶代数理论。 Fiore 和 Staton 使用替代代数和右 lambda 代数（二阶代数理论的特定实例）分别对跳跃效应和涉及代码指针堆栈的计算进行建模。进一步探索效应和二阶代数理论之间的联系是我将追求的一个有前途的研究方向。目标是找到产生效应的其他代数理论，反之亦然。首先，这种方法将有助于更好地理解效果的语义。从长远来看，效应和代数之间的联系可以为利用计算效应扩展编程演算提供一个通用框架。然后可以在高级通用编程语言之上实现这些扩展。在 ICT 研究主题中，该项目属于理论计算机科学领域的一部分，因为它采用了形式推理、逻辑概念和语义。该项目也是编程语言和编译器领域的一部分，因为其目的是更好地理解编程语言，并可能带来新的实现。