We consider the first order autonomous differential equation (ODE) ${\bf x}'={\bf f}({\bf x})$ where ${\bf f}: {\mathbb R}^n\to{\mathbb R}^n$ is locally Lipschitz. For ${\bf x}_0\in{\mathbb R}^n$ and $h>0$, the initial value problem (IVP) for $({\bf f},{\bf x}_0,h)$ is to determine if there is a unique solution, i.e., a function ${\bf x}:[0,h]\to{\mathbb R}^n$ that satisfies the ODE with ${\bf x}(0)={\bf x}_0$. Write ${\bf x} ={\tt IVP}_{\bf f}({\bf x}_0,h)$ for this unique solution. We pose a corresponding computational problem, called the End Enclosure Problem: given $({\bf f},B_0,h,\varepsilon_0)$ where $B_0\subseteq{\mathbb R}^n$ is a box and $\varepsilon_0>0$, to compute a pair of non-empty boxes $(\underline{B}_0,B_1)$ such that $\underline{B}_0\subseteq B_0$, width of $B_1$ is $<\varepsilon_0$, and for all ${\bf x}_0\in \underline{B}_0$, ${\bf x}={\tt IVP}_{\bf f}({\bf x}_0,h)$ exists and ${\bf x}(h)\in B_1$. We provide a complete validated algorithm for this problem. Under the assumption (promise) that for all ${\bf x}_0\in B_0$, ${\tt IVP}_{\bf f}({\bf x}_0,h)$ exists, we prove the halting of our algorithm. This is the first halting algorithm for IVP problems in such a general setting. We also introduce novel techniques for subroutines such as StepA and StepB, and a scaffold datastructure to support our End Enclosure algorithm. Among the techniques are new ways refine full- and end-enclosures based on a {\bf radical transform} combined with logarithm norms. Our preliminary implementation and experiments show considerable promise, and compare well with current validated algorithms.

翻译：我们考虑一阶自治微分方程(ODE) ${\bf x}'={\bf f}({\bf x})$，其中 ${\bf f}: {\mathbb R}^n\to{\mathbb R}^n$ 是局部 Lipschitz 连续的。对于 ${\bf x}_0\in{\mathbb R}^n$ 和 $h>0$，关于 $({\bf f},{\bf x}_0,h)$ 的初值问题(IVP)旨在判断是否存在唯一解，即满足该 ODE 且 ${\bf x}(0)={\bf x}_0$ 的函数 ${\bf x}:[0,h]\to{\mathbb R}^n$。记此唯一解为 ${\bf x} ={\tt IVP}_{\bf f}({\bf x}_0,h)$。我们提出一个相应的计算问题，称为终端包围问题：给定 $({\bf f},B_0,h,\varepsilon_0)$，其中 $B_0\subseteq{\mathbb R}^n$ 是一个区间向量（盒子），$\varepsilon_0>0$，要求计算一对非空盒子 $(\underline{B}_0,B_1)$，使得 $\underline{B}_0\subseteq B_0$，$B_1$ 的宽度 $<\varepsilon_0$，并且对于所有 ${\bf x}_0\in \underline{B}_0$，${\bf x}={\tt IVP}_{\bf f}({\bf x}_0,h)$ 存在且 ${\bf x}(h)\in B_1$。我们为此问题提供了一个完整的验证算法。在假设（承诺）对于所有 ${\bf x}_0\in B_0$，${\tt IVP}_{\bf f}({\bf x}_0,h)$ 均存在的前提下，我们证明了该算法的可停机性。这是在此类一般性设定下首个可停机的 IVP 问题算法。我们还为 StepA 和 StepB 等子程序引入了新技术，并采用了一种支撑性的脚手架数据结构来支持我们的终端包围算法。这些技术中包括基于{\bf 根式变换}结合对数范数来细化全包围和终端包围的新方法。我们的初步实现和实验显示出相当大的潜力，并且与当前验证算法相比表现良好。