线性函数方程的良展开式解

一、引言论证递归程序f=E(f)(1)特性的传统方法有结构归纳法(Bustall)和递归归纳法(McCarthy)等.1977年,Backus 在他的Turing 奖讲演中提出了函数式程序设计系统(即FP 系统),并指出可以发展一种程序代数来论证FP 程序(递归的或非递归的).这种代数方法的优点在于程序员可以直接使用程序设计语言本身陈述程序验证过程,并且不需要具有高深的数学知识.尤其重要的是这种代数方法的处理对象可以是一类程序而不是个别的程序,这就有可能导致许多关于     

函数型程序代数的方程求介

传統的von Neumann型語言,如FORTRAN、ALGOL等,和以λ—演算为基础的語言,如LISP等,均存在程序缺乏层次結构和理想的数学性質等一系列根本性缺陷。針对这种状况,John Backus在1977年接受Turing奖时提出了函数型程序設計(FP)系統。由于該系統对程序設計、程序驗証和計算机結构等可能产生的深远影响,因而引起国际計算机界的普遍重視。FP系統的一个突出优点是对于每个这样的系統均可結合一个程序代数,使得所有的程序,即FP系統的函数,构成該代数的变量域;所有的程序构造运算(program-forming operatiou),即FP系統的泛函型(functional form),构成該代数的运算。这样,程序便将成为理想的数学对象,并且无疑地将导致关于程序的結构和行为的一般定理的发現。