补充资料：程序理论

程序理论
theory of programs

程·65·型(集合)作为程序规约，而它们的元素就是满足规约的程序;用一组规则定义类型与其元素间的隶属关系，这些规则即是从规约产生程序的变换规则，又是一阶(直觉主义)逻辑的证明规则。因此，只要对给定的规约(逻辑命题)进行证明，就可以构造出符合此规约的程序。这样，程序规约、变换、验证都离于对规约的证明之中了。马丁洛夫理论的基本对象是a:A，其中A是一类型，a是类型A中的元素，称为A的居元。这个理论定义了几种基本类型:A~B，AxB，A+B，nx:声和凡:声，每种类型都由一组规则定义，这些规则确定了居元和类型间的关系。这个理论的基本对象a:A有多种解释，这些解释导致了它在程序设计和开发理论中的应用。例如:a:A可以解释为(居元:类型)、(证明:命题)、(程序:规约)等。以类型A~B为例，它有下述两条基本规则:、J了、.了，12子矛.‘、了r‘、x:A卜b:B触:.b:A一Bm:A~Bn:Amn:B 它们有三种解释: 解释1:(居元:类型)。规则(l)表示:若类型A有居元x可以推出类型B有居元b，则类型A~B有居元七.b。规则(2)表示:若类型A~B有居元m且类型A有居元n，则类型B有居元mn。其中，七.b，mn，m和n称为不项，前两者分别称为又-抽象和弄作用(见孟演算)。类型理论的重要结论是:给定典型居元a和类型A，可以在有限步内判断a是否为A的居元，这就是类型理论的强范式化性质。 解释2:(证明:命题)。采用直觉主义逻辑的观点，一个逻辑命题为真当且仅当存在此命题的证明。若把a:A解释为a是命题A的证明，把类型A~B解释为A蕴涵B。则规则(l)表示:若命题A有证明x可以推出命题B有证明b，则命题A~B有证明肚.b。规则(2)表示:若A‘B有证明m且命题A有证明n，则命题B有证明二n。若把规则(1)和(2)中的所有“证明”(类型的居元)去掉，它们就成为关于逻辑蕴牺的自然推理规则:些类型的规则就成为关于A(与)，V(或)，V(全称量词)和日(存在量词)的逻辑推理规则。这就是H创vard的“命题即类型”原则。 解释3:(程序:规约)。假定一阶逻辑语言作为规约语言，函数式语言作为程序语言，则不项:七、b，m。，m和n都将表示程序，而a:A可以解释为程序a满足规约A。规则(1)和(2)在这种情况下定义了程序与规约间的关系。规则(l)表示:若程序x满足规约A可以推出程序b满足规约B，则程序厄.b满足规约A~B。规则(2)表示:若程序m满足规约A~B，且程序。满足规约A，则程序mn满足规约B。

说明：补充资料仅用于学习参考，请勿用于其它任何用途。