The Functional Machine Calculus (Heijltjes 2022) is a new approach to unifying the imperative and functional programming paradigms. It extends the lambda-calculus, preserving the key features of confluent reduction and typed termination, to embed computational effects, evaluation strategies, and control flow operations. The first instalment modelled sequential higher-order computation with global store, input/output, probabilities, and non-determinism, and embedded both the call-by-name and call-by-value lambda-calculus, as well as Moggi's computational metalanguage and Levy's call-by-push-value. The present paper extends the calculus from sequential to branching and looping control flow. This allows the faithful embedding of a minimal but complete imperative language, including conditionals, exception handling, and iteration, as well as constants and algebraic data types. The calculus is defined through a simple operational semantics, extending the (simplified) Krivine machine for the lambda-calculus with multiple operand stacks to model effects and a continuation stack to model sequential, branching, and looping computation. It features a confluent reduction relation and a system of simple types that guarantees termination of the machine and strong normalization of reduction (in the absence of iteration). These properties carry over to the embedded imperative language, providing a unified functional-imperative model of computation that supports simple types, a direct and intuitive operational semantics, and a confluent reduction semantics.


翻译:函数式机器演算(Heijltjes 2022)是一种统一命令式与函数式编程范式的新方法。它扩展了λ演算,保留了合流归约和类型化终止的关键特性,以嵌入计算效应、求值策略和控制流操作。第一部分通过全局存储、输入/输出、概率和非确定性对顺序高阶计算进行了建模,并同时嵌入了按名调用与按值调用的λ演算,以及Moggi的计算元语言和Levy的按推送值调用。本文将该演算从顺序控制流扩展到分支与循环控制流。这使得能够忠实嵌入一个最小但完整的命令式语言,包括条件语句、异常处理和迭代,以及常量和代数数据类型。该演算通过简单的操作语义定义,它扩展了用于λ演算的(简化)Krivine机,通过多个操作数栈来建模效应,并通过一个延续栈来建模顺序、分支和循环计算。它具有一个合流的归约关系和一个简单类型系统,该系统保证了机器的终止性以及归约的强正规化(在无迭代的情况下)。这些性质延续到被嵌入的命令式语言中,从而提供了一个支持简单类型、直接直观的操作语义以及合流归约语义的统一函数式-命令式计算模型。

0
下载
关闭预览

相关内容

【2023新书】机器人,视觉和控制:Python第3版基本算法
专知会员服务
106+阅读 · 2023年5月21日
机器学习损失函数概述,Loss Functions in Machine Learning
专知会员服务
84+阅读 · 2022年3月19日
专知会员服务
54+阅读 · 2020年12月24日
综述:军事应用中使用的一些重要算法
专知
12+阅读 · 2022年7月3日
机器也能学会如何学习?——元学习介绍
AINLP
19+阅读 · 2019年9月22日
第二章 机器学习中的数学基础
Datartisan数据工匠
12+阅读 · 2018年4月5日
干货|掌握机器学习数学基础之优化[1](重点知识)
机器学习研究会
10+阅读 · 2017年11月19日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Arxiv
0+阅读 · 2月3日
Arxiv
0+阅读 · 1月28日
Arxiv
0+阅读 · 1月19日
Arxiv
0+阅读 · 1月5日
VIP会员
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员