Strategies on functional languages

函数式语言策略

• 批准号: 11680352
• 负责人: SAKAI Masahiro
• 金额: $ 2.18万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 1999
• 资助国家: 日本
• 起止时间: 1999 至 2002
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-11680352/
• 关键词: term rewriting system; normalizing strategy; functional language

This research is toward removing gaps that prevent from applying results of term rewriting systems (TRSs for short) to factional languages. The following results were obtained ;(1) Only TRSs having few rules can be decided whether they are NV-sequential in realistic execution time. The execution time of the calculating an index of a given term and a TRS is similar to the decision problem.(2) We extended the notion of root indexes of TRSs to TRSs with priorities and construct a prototype system that efficiently caliculate indexes for head normal forms of strongly sequential priority TRSs.(3) The strategy that reduce needed redex is normalizing.(4) We showd a class of higher-order TRSs in which the dependency pair method, a mecanized proof technique of termination, is effective.(5) The leftmost innermost reduction strategy is normalizing for terminating, right-linear and root over-lapping TRSs.

这项研究是为了消除差距，阻止应用的结果项重写系统（简称TRS）的派别语言。结果表明：（1）只有规则数较少的TRS才能在实际执行时间内判定其是否为NV-序列。计算给定项的索引和TRS的执行时间类似于决策问题。(2)我们将TRS的根索引的概念扩展到具有优先级的TRS，并构造了一个原型系统，有效地计算强顺序优先级TRS的头范式的索引。(3)减少所需Redex的策略是正常化。(4)本文给出了一类高阶TRS，其中依赖对方法是一种有效的终止性的机械化证明技术。(5)对于终止、右线性和根重叠的TRS，最左最内的约简策略是归一化的。

项目成果

洪順姫, 酒井正彦, 坂部俊樹: "メタ項書換え計算における規則中に規則を含む直交メタ項の合流性"コンピュータソフトウェア. 17・6. 47-51 (2000)

Junhi Hong、Masahiko Sakai、Toshiki Sakabe：“包含元项重写计算中的规则的正交元项的汇合”计算机软件 17・6。

粕谷英人, 酒井正彦, 阿草清滋: "項書換え系におけるディセンダントと頭必須書換えの頭正規化性"電子情報通信学会技術報告. COMP2002. 65-72 (2001)

Hideto Kasuya、Masahiko Sakai、Kiyoji Asa：“后代的头部规范化和术语重写系统中所需的头部重写”IEICE 技术报告 65-72 (2001)。

西田直樹, 酒井正彦, 坂部俊樹: "右辺のみに現れる変数を持つ項書換え系の計算モデル"コンピュータソフトウェア. (印刷中). (2003)

Naoki Nishida、Masahiko Sakai、Toshiki Sakabe：“变量仅出现在右侧的术语重写系统的计算模型”计算机软件（2003 年）。

M.Sakai, K.Kusakari: "On New Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems"The International Workshop on Rewriting in Proof and Computation, Sendai, Japan, RIEC Tohoku University. RPC'01. 176-187 (2001)

M.Sakai、K.Kusakari：“关于证明高阶重写系统终止的新依赖对方法”国际证明和计算重写研讨会，日本仙台，RIEC 东北大学。

N.Nishida, M.Sakai, T.Sakabe: "Generation of a TRS Implementing the Imverses of Pure Treeless Function"Computer Software. Vol.20, No.2. 29-33 (2002)

N.Nishida、M.Sakai、T.Sakabe：“生成实现纯无树函数逆的 TRS”计算机软件。