著者

櫻田 英樹

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.41, no.9, pp.8-24, 2000-11-15

---

本研究では,プログラミング言語における文脈と環境の関係を調べる.プログラミング言語において文脈とは,穴を持つプログラムのことである.文脈はプログラミング言語の操作的意味論を定義するときなどに用いられる.橋本,大堀(1996)は文脈をファーストクラスのオブジェクトとして持つ型付き ${エlambda}$ 計算を考えた.ファーストクラスの文脈を用いて,モジュールシステムやモバイルコードを柔軟に扱うことができると期待されている.一方,プログラミング言語において環境とは,変数の名前とその値の組の集合のことである.環境は局所的束縛を扱うためにしばしば用いられる.LISPのletなどは環境を作り,その中でプログラムを評価するものである.環境をファーストクラスのオブジェクトとして持つような ${エlambda}$ 計算はいくつかあり,佐藤,Burstall,桜井(1999)による ${エlambda}{エvarepsilon}$ はその1つである.ファーストクラスの環境を用いてオブジェクト指向プログラミングなどを扱うことができると期待されている.本研究では,橋本,大堀の型付文脈計算を,佐藤,Burstall,桜井の ${エlambda}{エvarepsilon}$ を用いて解釈し,解釈の健全性を証明した.また,これにより型付文脈計算が強正規性を満たすことが分かった.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.