证明网络图归约优化系统的研制

在Asperti及Lavane的合法通道中界定了一类“强正则通道”，并证明：该类通道所代表的归约过程既是优化归约过程。反过来，任一优化归约过程所形成的合法通道必定是强正则通道。这样，证明网络上的优化归约的寻求，就可以通过在图上的强正则通道的寻求来达到。而通道的寻求是可以用算法来实现的。在我们建立的系统Interaction through Context中实现了优化归约。我们提出了通过内框架交互来检验函词式程序的协调性的方法。此方法大大地优于Jacoppini的判定法则。同时我们对与此相关的理论问题，易项的分类问题做了大量的研究。与加州大学Baker合作，在代数等式系有穷公理化领域里取得国际领先的重大成果：发现一个至今为止是国际上最广义的有穷基定理。