Lawson紧的代数L-domain递归方程的逻辑形式

Lawson Compact Algebraic L-domain Equations in Logical Form

本文的目的是为Lawson紧的代数L-domain递归方程及其解提供一种逻辑刻画。基于N-序列演算上的子系统关系,证明了N-序列演算之集是定向完备的,并在这一定向完备偏序集上引入了三种连续构造算子:提升,联结和以及分离和。从而求解domain结构递归方程的问题可归结为如何构建连续映射的不动点。

The main purpose of this paper is to provide a logical approach to solving Lawson compact algebraic L-domain equations.The method is based on the subsystem relation between N-sequent calculi.This makes a directed complete poset of N-sequent calculi.Some domain constructors like lifting,coalesced sum and separated sum can be made continuous on this directed complete poset.Thus the problem of solving recursive domain equation reduces to how to construct the fixed point of continuous mapping.