文脈計算の環境計算による解釈

• Item type: Trans(1)
• 公開日: 2000-11-15
• タイトル: 文脈計算の環境計算による解釈
• タイトル / 言語: en
• タイトル: An Interpretation of a Context Calculus in an Environment Calculus
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: NTTコミュニケーション科学基礎研究所
• 著者所属(英): en
• 著者所属(英): NTT Communication Science Laboratories
• 著者名: 櫻田, 英樹
• 著者名(英): Hideki, Sakurada
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本研究では，プログラミング言語における文脈と環境の関係を調べる．プログラミング言語において文脈とは，穴を持つプログラムのことである．文脈はプログラミング言語の操作的意味論を定義するときなどに用いられる．橋本，大堀(1996)は文脈をファーストクラスのオブジェクトとして持つ型付き ${ｴlambda}$ 計算を考えた．ファーストクラスの文脈を用いて，モジュールシステムやモバイルコードを柔軟に扱うことができると期待されている．一方，プログラミング言語において環境とは，変数の名前とその値の組の集合のことである．環境は局所的束縛を扱うためにしばしば用いられる．LISPのletなどは環境を作り，その中でプログラムを評価するものである．環境をファーストクラスのオブジェクトとして持つような ${ｴlambda}$ 計算はいくつかあり，佐藤，Burstall，桜井(1999)による ${ｴlambda}{ｴvarepsilon}$ はその1つである．ファーストクラスの環境を用いてオブジェクト指向プログラミングなどを扱うことができると期待されている．本研究では，橋本，大堀の型付文脈計算を，佐藤，Burstall，桜井の ${ｴlambda}{ｴvarepsilon}$ を用いて解釈し，解釈の健全性を証明した．また，これにより型付文脈計算が強正規性を満たすことが分かった．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We investigate the relationship between contexts and environments in programming languages. In programming languages, a context is a program with a hole. We often use contexts in defining operational semantics of programming languages. Hashimoto and Ohori (1996) have studied a typed context calculus, a typed ${ｴlambda}$-calculus with first-class contexts. We expect that we can build flexible module systems using first-class contexts. On the other hand, an environment in programming languages is a set of variable-value tuples. We use environments to express local bindings. For example, ``{ｴtt let}'' construct in LISP creates an environment and evaluates a program in it. There are several works on ${ｴlambda}$-calculus with first-class environments. ${ｴlambda}{ｴvarepsilon}$ by Sato, Sakurai and Burstall (1999) is one of them. We expect that first-class environments are useful for object-oriented programming. In this work, we develop an interpretation of Hashimoto-Ohori's typed context calculus in ${ｴlambda}{ｴvarepsilon}$. We prove its soundness and show that the context calculus is strongly normalizing.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 41, 号 SIG09(PRO8), p. 8-24, 発行日 2000-11-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会