This work continues the development of an intensional approach to computability initiated in previous work, in which programs and computations, rather than functions, constitute the primary objects of study. In this setting, models of computation are described as monoid actions on a configuration space, and programs as dynamical systems constrained by this action. Within this framework, we introduce a formal notion of algorithm as a finite directed graph whose edges are labelled by partial maps over an abstract data structure. This definition separates control from data, representing the former as a graph and the latter as an algebra of operations. We then define what it means for a program, in a given model of computation, to implement such an algorithm, by requiring a correspondence between computational steps and labelled transitions that preserves the induced transformations on representations of data. This yields a precise notion of implementation and situates algorithms as abstract partial specifications of computational behaviour.
翻译:本文延续了前期工作中启动的关于可计算性的内涵式方法,在该方法中,程序与计算(而非函数)构成主要研究对象。在此框架下,计算模型被描述为配置空间上的幺半群作用,而程序则被描述为受此作用约束的动力系统。基于这一框架,我们引入算法的形式化概念:一种有向有限图,其边由抽象数据结构上的部分映射标记。该定义将控制与数据分离,将前者表示为图、后者表示为操作代数。随后,我们定义了在给定计算模型中,程序实现此类算法的含义:要求计算步骤与标记转移之间存在对应关系,且该关系保持数据表示上的诱导变换。这为实现提供了精确的定义,并将算法定位为计算行为的抽象部分规范。