一句话：用域论构造有限可生成子集的可计算凸包映射，并导出其谓词变换器。
论文研究计算几何中表示部分或不精确点的非空紧凸子集构成的 domain。凸包映射由内凸包与外凸包以 domain 论方式给出；作者针对有限个凸多面体作为部分点的情形提出计算内凸包的实际算法，并引入 pre-inner support function，使其凸包在一般情形下给出内凸包的支撑函数。随后证明凸包映射是 Scott 连续的，可扩展到由底层 domain 的 Plotkin power domain 表示的有限可生成子集，从而首次计算分形几何中迭代函数系统吸引子的凸包。最后，作者按给定后条件的最弱前置条件意义推导凸包映射的程序逻辑，并证明凸包谓词变换器是可计算的。
We consider the domain of non-empty convex and compact subsets of a finite dimensional Euclidean space to represent partial or imprecise points in computational geometry. The convex hull map on such imprecise points is given domain-theoretically by an inner and an outer convex hull. We provide a practical algorithm to compute the inner convex hull when there are a finite number of convex polytopes as partial points. A notion of pre-inner support function is introduced, whose convex hull gives the support function of the inner convex hull in a general setting. We then show that the convex hull map is Scott continuous and can be extended to finitely generable subsets, represented by the Plotkin power domain of the underlying domain. This in particular allows us to compute, for the first time, the convex hull of attractors of iterated function systems in fractal geometry. Finally, we derive a program logic for the convex hull map in the sense of the weakest pre-condition for a given post-condition and show that the convex hull predicate transformer is computable.
DOI 原文 ·
@inproceedings{paperbot4974,
title = {The convex hull of finitely generable subsets and its predicate transformer},
author = {Mohammad Javad Davari and Abbas Edalat and Andre Lieutier},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785680}
}