HOL中的时钟定义

摘要：

许多潜在的非终止函数不能直接在全函数逻辑中定义，如HOL。对此，一个众所周知的解决方案是使用时钟来定义非终止函数，该时钟强制在某个求值深度处终止。这样的时钟定义通常是不赞成和避免的，因为时钟被认为是额外的混乱。在这篇简短的论文中，我们解释了添加时钟的不同方法，有些方法比其他方法侵入性更小。我们的贡献是一种技术，即使在最大限度地减少使用的时钟机制，终止证明保持简单。我们的例子是程序设计语言的语义解释器的定义，即所谓的函数大步语义。

英文摘要：

Many potentially non-terminating functions cannot be directly defined in a logic of total functions, such as HOL. A well-known solution to this is to define non-terminating functions using a clock that forces termination at a certain depth of evaluation. Such clocked definitions are often frowned upon and avoided, since the clock is perceived as extra clutter. In this short paper, we explain that there are different ways to add a clock, some less intrusive than others. Our contribution is a technique by which termination proofs are kept simple even when minimising the use of the clock mechanism. Our examples are definitions of semantic interpreters for programming languages, so called functional big-step semantics.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。