2018-01-22 環境、引数、パラメータ 高次圏論 プログラム意味論 論理 トランスフォーマーを考えると、定義体の内部で使う名前の供給源として、 名前は環境から供給される(名前は環境内のモノを参照する) 名前は引数から供給される(名前は引数内のモノを参照する) 名前はパラメータから供給される(名前はパラメータ内のモノを参照する) がある。ここで、引数とパラメータは区別している。引数は定義式内の自由変数。パラメータはラムダ束縛された変数。環境は暗黙に仮定するが、明示的に引数にしてもよい。環境と引数は相互に移りあえる。パラメータはラムダ変数のことなので、カリー同型により引数に直すことができる。ここらの相互変換が出来ることが(なにかの)鍵になっているような気がする。