公式即程序
计算机科学中的逻辑
2007-05-23 v1 符号计算
摘要
我们在此给出基于可满足性构造性解释（相对于固定但任意的解释）的一阶逻辑计算解释。在该方法中，公式本身就是程序。这与所谓的公式即类型（formulas as types）方法形成对比，后者中公式的证明是可作为程序的带类型项。这种计算视角受逻辑编程和约束逻辑编程启发，但在若干关键方面与之不同。我们认为公式即程序产生了一种现实的编程方法，并已在其实现的编程语言 ALMA-0（Apt 等人）中得以实现，该语言结合了命令式与逻辑编程的优点。此处报告的工作也可用于推理不包含破坏性赋值的非递归 ALMA-0 程序的正确性。
引用
@article{arxiv.cs/9811017,
title = {Formulas as Programs},
author = {Krzysztof R. Apt and Marc Bezem},
journal= {arXiv preprint arXiv:cs/9811017},
year = {2007}
}
备注
34 pages, appears in: The Logic Programming Paradigm: a 25 Years Perspective, K.R. Apt, V. Marek, M. Truszczynski and D.S. Warren (eds), Springer-Verlag, Artificial Intelligence Series