項書換え計算モデルのプログラミングへの応用

项重写计算模型在编程中的应用

• 批准号: 03235201
• 负责人: 井田 哲雄
• 金额: $ 1.28万
• 依托单位: University of Tsukuba
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 1991
• 资助国家: 日本
• 起止时间: 1991 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-03235201/
• 关键词: 項書換之計算系; ナロ-イング; 関数・論理型プログラミング

関数、論理型言語を融合する宣言型言語の計算モデルとして、遅延ナロ-イング計算系と呼ばれる計算系を定義した。この計算系は、条件付き項書換え系に基づくものである。反駁による証明を計算の機構とし、証明の過程で値が必要となった関数項のみをナロ-イングにより簡約するものである。この計算系はナロ-イングをいくつかの基本的な推論規則に分解することで、等式の反駁の高速な実行を可能にしている。この計算系関して行った研究内容を以下に示す。1.遅延ナロ-イング計算系の完全性の証明我々が答とみなすすべての項が答として確かに得られることを示した。2.関数・論理型言語の設計遅延ナロ-イング感算系に基づく言語を設計し、さらにその処理系を実装した。3.上記言語の抽象機械の設計上記言語の処理系は、抽象機械をシミュレ-トすることによって動作している。この抽象機械を、遅延ナロ-イング計算系の推論規則の振舞いを解析することによって、得た。また、プログラムから抽象機械の命令列へと翻訳するコンパイラも作成した。4.正則項書換え系の正規化手続きの実現への応用遅延ナロ-イング計算系を応用して、正則項書換え系の正規化簡約系を得る方法を示した。

The computational system of declarative speech is defined by the fusion of relational and logical speech. This calculation is based on the condition that the term is changed. Rebuttal of the proof of the calculation of the mechanism, proof of the process is necessary to determine the number of terms of the proof of the structure of the proof. This calculation is based on the basic inference rules of the equation, and the fast implementation of the equation. The research contents of this calculation system are shown below. 1. Proving the completeness of the computational system of delay and delay; 2. The design of logical speech is based on the implementation of speech design and processing systems. 3. On the design of abstract speech machinery, on the processing of speech, abstract machinery, on the design of speech machinery, on the design of speech machinery. The abstract mechanical analysis, delay analysis and calculation of the inference rules of the vibration analysis The command line of abstract machinery is made up of a number of components. 4. A method for obtaining the normalized reduced system of regular term transformation is presented.