一句话：提出词典序格结构上的不动点定理，统一非单调形式体系的最小不动点语义。
针对非单调形式体系（如正规逻辑程序、带否定的高阶逻辑程序、布尔文法）缺乏统一语义工具的问题，本文引入词典序格结构：格元素可视为分层实体，序关系按层词典序比较。允许函数整体非单调，但在每一层内保持受限单调性。作者证明此类函数总有最小不动点，且该点是其最小前不动点；其前不动点集与后不动点集均为完备格。当结构退化为单层时，结果即经典 Knaster-Tarski 定理。该工作简化并推广近期非单调不动点理论，为相关形式体系的语义研究提供通用工具。
We introduce the notion of a lexicographic lattice structure, namely a lattice whose elements can be viewed as stratified entities and whose ordering relation compares elements in a lexicographic manner with respect to their strata. These lattices arise naturally in many non-monotonic formalisms, such as normal logic programs, higher-order logic programs with negation, and boolean grammars. We consider functions over such lattices that may overall be non-monotonic, but retain a restricted form of monotonicity inside each stratum. We demonstrate that such functions always have a least fixed point which is also their least pre-fixed point. Moreover, we prove that the sets of pre-fixed and post-fixed points of such functions, are complete lattices. For the special case of a trivial lexicographic lattice structure whose elements essentially consist of a unique stratum, our theorem gives as a special case the well-known Knaster-Tarski fixed point theorem. Moreover, our work considerably simplifies and extends recent results on non-monotonic fixed point theory, providing in this way a useful and convenient tool in the semantic investigation of non-monotonic formalisms.
DOI 原文 ·
@inproceedings{paperbot5489,
title = {A Fixed Point Theorem on Lexicographic Lattice Structures},
author = {Angelos Charalambidis and Giannos Chatziagapis and Panos Rondogiannis},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394797}
}