Automated Complexity Analysis for Term Rewriting

术语重写的自动复杂性分析

• 批准号: 20800022
• 负责人: HIROKAWA Nao
• 金额: $ 1.62万
• 依托单位: Japan Advanced Institute of Science and Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (Start-up)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2009
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20800022/
• 关键词: 項書き換え; 計算モデル; 計算量; 情報基礎

探索やソートアルゴリズムを開発したとき、「入力の大きさに対しどれくらいの速度(ステップ数)で動作するか」という自然な疑問が生じる。現在に至るまで時間的計算量は、プログラムごとに手作業で解析するものと認識されていた。本研究では、関数型プログラムの計算モデルである項書き換え系に対して、解析を自動化する強力な理論を構築した。さらにそれに基づく計算量自動解析ツールを実装した。既存手法との比較実験を行った結果、解析精度の劇的な向上が確認された。

Explore the open source of the software,"The input force is large, the speed is small, the movement is small," and the natural question arises. The amount of time that has elapsed since then has been calculated. In this study, we construct a powerful theory for the calculation and analysis of mathematical models. The basic calculation quantity is automatically resolved. Comparison of existing methods and results, analytical accuracy and upward validation

项目成果

Uncurrying for Termination. In Proceedings of the 15th International Conferences on Logic for Programming

取消柯里化以终止。

• 发表时间: 2008
• 作者: Nao Hirokawa;Aart Middeldorp;Harald Zankl
• 通讯作者: Harald Zankl

Complexity, Graphs, and the Dependency Pair Method

复杂性、图形和依赖对方法

• 发表时间: 2008
• 作者: Nao Hirokawa;Georg Moser
• 通讯作者: Georg Moser

The Subterm Criterion in Complexity Analysis

复杂性分析中的子项准则

• 发表时间: 2009
• 作者: Nao Hirokawa;Georg Moser
• 通讯作者: Georg Moser

Uncurrying for Termination

取消柯里化以终止

• 发表时间: 2008
• 作者: Nao Hirokawa;Aart Middeldorp;Harald Zankl
• 通讯作者: Harald Zankl

電子情報通信学会 知識ベース 7群1編「ソフトウェア基礎」2章「定理証明と検証法」3節「SAT」執筆

IEICE 知识库，第 7 组，第 1 卷，“软件基础知识”，第 2 章，“定理证明和验证方法”，第 3 节，“SAT”写作

• 发表时间: 2010
• 作者: Nao Hirokawa;Georg Moser;廣川直;廣川直
• 通讯作者: 廣川直