...
首页> 外文期刊>Science of Computer Programming >Type-2 effectivity in abstract state machines for algorithms with exact real arithmetic
【24h】

Type-2 effectivity in abstract state machines for algorithms with exact real arithmetic

机译:具有精确实数算法的抽象状态机中的2类有效性

获取原文
获取原文并翻译 | 示例
           

摘要

Computations with real numbers are decisive for all scientific and technical applications, in particular cyber-physical systems, and precision in the results is essential for quality and safety. The type-2 theory of effectivity (TTE) is a well established theory of computability on infinite strings, which can be used to represent real numbers by rapidly converging Cauchy sequences, on top of which standard operations such as addition, multiplication, division, exponentials, trigonometric functions, etc. can be defined. In this paper we develop an extension of Abstract State Machines (ASMs) handling streams in an incremental way in accordance with TTE. This enables defining a data type Real as part of the background structure and based on this exact computation with real numbers. Output can be generated at any degree of precision by exploring only sufficiently long prefixes of the representing Cauchy sequences. We then outline an ASM development process that starts from a specification of an algorithm using Real, proceeds by making the rational elements of the Cauchy sequences explicit in a refinement, reconsiders this refined specification as a concurrent ASM, where each agent cares about computation up to some precision, and finally, based on a detailed analysis of the required precision, prunes the concurrent ASM down to an ASM that guarantees a sufficient level of precision in the outputs. In doing so, backward precision propagation replaces the common forward error propagation that is common for implementations exploiting floating point arithmetic. (C) 2019 Elsevier B.V. All rights reserved.
机译:实数计算对于所有科学和技术应用(尤其是网络物理系统)都是决定性的,结果的精确性对于质量和安全性至关重要。类型2有效性理论(TTE)是对无穷字符串的一种公认的可计算性理论,可以通过快速收敛柯西序列来表示实数,并在其上进行加,乘,除,指数等标准运算,三角函数等可以定义。在本文中,我们根据TTE开发了以增量方式处理流的抽象状态机(ASM)的扩展。这使得可以将数据类型Real定义为背景结构的一部分,并基于具有实数的精确计算。通过仅探查代表柯西序列的足够长的前缀,可以以任何精确度生成输出。然后,我们概述了一个ASM开发过程,该过程从使用Real的算法规范开始,通过细化Cauchy序列的有理元素来进行改进,将这种改进的规范重新考虑为并发ASM,其中每个代理都关心计算直到一定的精度,最后,基于对所需精度的详细分析,将并发ASM缩减为一个ASM,以保证输出中足够的精度。这样,后向精度传播将替换使用浮点算法的实现中常见的常见前向误差传播。 (C)2019 Elsevier B.V.保留所有权利。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号