A study on duality-based program transformation

(1)从多态λ微积分到存在微积分的伽罗瓦嵌入：我们定义了一个基于对偶的从多态λ微积分到存在微积分的程序转换。然后在翻译的基础上，证明了微积分之间存在伽罗瓦连接，并证明了从多态λ微积分到存在微积分的伽罗瓦嵌入。(2)无类型λ - μ微积分和抽象机的健全完备的ops -翻译：我们提供了无类型λ - μ微积分到带满射对λ -微积分的健全完备的ops -翻译。在cps转换之后，我们还介绍了一个抽象机器，它执行cps代码并显式地处理与替换相关的环境。(3)伴随cps -平移：我们定义了具有可拓性的多态λ微积分的基于对偶的程序变换（cps -平移）。然后，在约简的自反闭包和及物闭包所定义的前置顺序下，可以将翻译解释为伴随式。也就是说，逆可以由主下集的逆像在预阶下的最大元素来定义，因此，给定基于对偶的平移，逆平移可以唯一确定。作为这个项目的副产品，我们引入了一种新的类型系统，据我们所知，称为存在演算。该演算对抽象数据类型进行建模，并与多态λ演算具有伽罗瓦联系。我们希望通过揭示微积分的基本性质，给以多态微积分为子系统的微积分提供一个新的有趣的视角。

(1) Galois embedding from polymorphic lambda-calculus into existential calculus :We have defined a duality-based program transformation from polymorphic lambda-calculus into existential calculus. Then under the translation, it is shown that there exists a Galois connection between the calculi, and moreover a Galois embedding from polymorphic lambda-calculus into existential calculus.(2) Sound and complete OPS-translation for type-free lambda-mu-calculus and abstract machine :We have provided a sound and complete CPS-translation from type-free lambda-mu-calculus into lambda-calculus with surjective pair. Following the CPS-translation, we also introduced an abstract machine which executes CPS-codes and explicitly handles environment associated with substitution.(3) CPS-translation as adjoint :We have defined the duality-based program transformation (CPS-translation) for polymorphic lambda-calculus with extensionality. Then under the pre-order defined by the reflexive and transitive closure of the reduction, the translation can be expounded as an adjoint. That is, an inverse can be defined by the maximum element of an inverse image of a principal down-set under the pre-order, so that given the duality-based translation the inverse translation can be uniquely determined.As a by-product of this project, we have introduced a new type system, as far as we know, called an existential calculus. This calculus models abstract data types and has a Galois connection to polymorphic lambda-calculus. We hope that revealing the fundamental property of the calculus gives a new and interesting viewpoint to calculi involving polymorphic calculus as a subsystem.