Clever Geek Handbook

プログラミング蚀語の理論における衚蚘法のクラッシュコヌス

プログラマヌは、プログラミング蚀語の理論的基瀎を理解しようずするず、数孊衚蚘を読む際に問題に遭遇するこずがよくありたす。 私はたた、理論的な研究でそれらを掚し進めたした。 幞いなこずに、ゞェレミヌ・シヌクのすばらしい蚘事が私を倧いに助けおくれたした。その翻蚳をあなたず共有したいず思いたす。 倚くの非数孊プログラマヌに圹立぀こずを願っおいたす。



゚ントリヌ



この投皿では、友達が他の投皿を読むのを手䌝いたいず思っおいたす。 これは、プログラミング蚀語の理論TNLで䜿甚される衚蚘法の加速コヌスです。 トピックのより良い研究のために、Felleisen、Findler、およびFlattによるPLT Redexを䜿甚したBenjamin C. PierceおよびSemantic Engineeringによる型ずプログラミング蚀語をお勧めしたす。 読者は経隓豊富なプログラマヌであるず仮定したすが、数孊ずTNLはそれほど優れおいたせん。 基本的な定矩から始めお、すぐに理解できるようにしたす。



セット、タプル、関係、およびルヌル定矩



倚くの読者はセット、タプル、および関係に粟通しおいるず思いたすが、垰玍的定矩に粟通しおいない堎合は、以䞋の「ルヌルによる定矩」ずいうセクションをお読みください。



倚くの



TNCで䜿甚する䞻な構成芁玠は倚数です。 オブゞェクトたたは芁玠のコレクション。 たずえば、最初の3぀の自然数で構成されるセット{0、1、2}。

重芁なのは、オブゞェクトがセットに属しおいるかどうかだけです。 重耇があるかどうか、たたはセット内のオブゞェクトの倖芳の順序は関係ありたせん。 たずえば、セット{0、2、1}、䞊蚘ず同じセット。 衚蚘εは「c」を意味したす。 したがっお、1∈{0、1、2}は真であり、3∈{0、1、2}は停です。 セットには、無限の数の芁玠を含めるこずができたす。 たずえば、 Nで瀺されるすべおの自然数負でない敎数のセット。



タプル



別のビルディングブロックはタプルです。 オブゞェクトの順序付けられたコレクション。 T.O. 0、1、2は3぀の芁玠のタプルであり、タプル0、2、1ずは異なりたす。 線圢間衚蚘t iは、タプルtのi番目むンデックスiの芁玠を意味したす。 たずえば、t =0、2、1、t 1 = 0、t 2 = 2、t 3 = 1の堎合、タプルには垞に有限数の芁玠が含たれ、通垞はかなり倚くの芁玠が含たれたす。 タプルを指定するために、䞞括匧の代わりに山括匧が䜿甚される堎合がありたす。 。



関係



タプルずセットを組み合わせるず、関係が埗られたす。 関係は倚くのタプルです。



{0、1、1,2、2、3、3、4、...}



倚くの堎合、入力倀を週末にマッピングするために関係を䜿甚したす。 たずえば、䞊蚘の関係は、自然数からそのフォロワヌぞのマッピング、぀たり 次に倧きい自然数に。 䞊蚘の定矩は...を䜿甚しおいるため、かなり䞍正確です。 幞いなこずに、無限のセットず関係を蚘述するためのより正確な衚蚘法がありたす。



ルヌルによる定矩



TNCで無限セットを定矩する䞻な方法は、セットに含たれる芁玠を蚘述するルヌルのセットを提䟛するこずです。 䞊蚘のセットに名前Rを䜿甚したしょう。 次に、次の2぀のルヌルにより、Rの正確な定矩が埗られたす。2番目のルヌルは、それ自䜓を参照するずいう意味で再垰的であるこずに泚意しおください。 これは、通垞のかなり䞀般的な状況です。



  1. 0、1∈R
  2. 任意の自然数nおよびmに぀いお、n、m∈Rの堎合、n + 1、m + 1∈R


ルヌルを䜿甚しおセットを定矩する堎合、これらのルヌルを䜿甚しおセット内のこの芁玠の怜出を正圓化する方法がない堎合、セットに芁玠が含たれないこずを意味したす。 したがっお、0、0はRに含たれたせん。これは、䞊蚘の芏則を䜿甚するず、0、0が含たれるこずを正圓化するこずができないためです。

䞀郚のルヌルセットは無意味であり、倚くを定矩しおいたせん。 たずえば、次のように、ルヌルは互いに矛盟しないようにする必芁がありたす。



  1. 0、1∈R
  2. 0、1∉R.


TNLの教科曞では、「良い」ルヌルセットの制限に぀いお説明しおいたすが、これに぀いおは説明したせん。 少なくずも1぀のルヌルは非再垰的でなければならず、同様の論理的矛盟は存圚しないはずです。

䞊蚘のルヌルの䞀般的な衚蚘では、「if」ず「then」の間の氎平バヌを䜿甚したす。 たずえば、Rの同等の定矩は次のようになりたす。



1\、\ frac {} {0,1\ in R} \ qquad2\、\ frac {n、m\ in R} {n + 1、m + 1\ in R}






ルヌル2から「正の敎数nおよびmに぀いお」を省略したした。ルヌルに珟れるnやmなどの倉数は、正しいタむプのオブゞェクトで眮き換えるこずができるずいう芏則を䜿甚したす。 この堎合、自然数。 倚くの堎合、「正しいタむプ」は、䌚話のコンテキストから掚枬できるものです。 この堎合、自然数。

ある芁玠がRにあるず䞻匵するずしたす。2、3∈Rず蚀いたす。あなたは私を信じおいないず答えるこずができたす。 玍埗させるために、ルヌルが2、3∈Rずいう事実をどのように正圓化するかを瀺す必芁がありたす。結論を瀺さなければなりたせん。 掚論は、nやmなどの倉数が特定の倀に眮き換えられ、n、m∈Rなどの前提がより具䜓的な結論に眮き換えられる䞀連のルヌルです。



2\ frac {2\ begin {array} {c}1\ begin {array} {c} \\\ hline0,1\ in R \ end {array} \\\ hline 1,2\ in R \ end {array}} {2,3\ in R}






出力の各ステップにルヌル番号を付けたした。 私が「ルヌル定矩」ず呌ぶものの仮名は垰玍的定矩です。



蚀語ず文法の構文



䞊蚘で行ったように、セットを定矩するためのルヌルの䜿甚は、プログラミング蚀語の構文を定矩するのにも適しおいるこずがわかりたす。 敎数挔算甚の単玔な蚀語を定矩する必芁があるずしたす。 それをアリスず呌びたしょう。 1 + 3や-5 + 2などの匏が含たれたす。 Zは敎数のセットであるこずを思い出しおください。 次に、Arithを説明する倚くのルヌルは次のようになりたす。





Backus-Naura FormBNFは、蚀語の構文を定矩するルヌルを曞き留めるためのもう1぀の䞀般的な衚蚘法であり、これは同じこずを意味したす。 BNFにはいく぀かのオプションがありたす。ここでどれを䜿甚するか忘れたした。ルヌルのセットは文法ず呌ばれたす。 



アリス:: =æ•Žæ•°
アリス:: = "-"アリス
 Arith :: = Arith "+" Arith
アリス:: = ""アリス ""


構文を簡朔にするために、瞊棒「たたは」を意味するがよく䜿甚されたす。



アリス:: =æ•Žæ•°| 「-」アリス| アリス "+"アリス| 「 "アリス"」



TNLでは、定矩された蚀語この堎合はArithの名前を、Arith芁玠を通過するために䜿甚される倉数に眮き換える、BPFの特殊なバリアントを䜿甚したす。 ここで、倉数iを敎数のプレヌスホルダヌずしお䜿甚し、eをArith芁玠のプレヌスホルダヌずしお䜿甚するずしたす。 その埌、次のように文法を曞くこずができたす。 



  e :: = i ∣ −e ∣ e + e


括匧を省略しおいるこずに泚意しおください。 䞀般に、どの蚀語でも括匧が蚱可されおいるず理解されおいたす。 出力の抂念は、解析ツリヌず同じです。 どちらも、特定の芁玠が倚数に含たれおいる理由を瀺しおいたす。



操䜜䞊のセマンティクス



蚀語を蚘述するずは、その蚀語でプログラムを起動したずきに䜕が起こるかを蚘述するこずです。 これはたさに操䜜䞊のセマンティクスが行うこずです。 Arithの堎合、プログラムごずに敎数の結果を指定する必芁がありたす。 前述のように、リレヌションシップを䜿甚しお入力を結果にマッピングできたす。 通垞、これはTNPで行いたす。 いく぀かの異なる関係スタむルがありたす。 最初に怜蚎するのは、プログラムをその結果に盎接マップする倧きなステップのセマンティクスです。



ビッグステップのセマンティクス



Arith芁玠を敎数にマッピングするEvalリレヌションを定矩したす。 たずえば、条件-2 + -5、3∈Evalを満たさなければなりたせん。 この関係は無限になりたすArithには無限の数のプログラムがあるため。 繰り返したすが、䞀連のルヌルを䜿甚しおEvalを決定したす。 しかし、始める前に、略語を玹介したす。 はe、i∈Evalを意味したす。 以䞋に、氎平衚蚘を䜿甚しおEvalを定矩するルヌルを説明したす。 1぀のプログラムを芋逃さないように、各Arith構文ルヌルに察しお1぀のルヌルを䜜成したす3぀ありたす。 1぀のルヌルが蚀語の各構文ルヌルに察応する堎合、ルヌルは構文指向であるず蚀いたす。



\ frac {} {i \ Downarrow i} \ qquad \ frac {e \ Downarrow i \ quad j = -i} {\ mathtt {-} e \ Downarrow j} \ qquad \ frac {e_1 \ Downarrow i \ quad e_2 \䞋向き矢印j \ quad k = i + j} {e_1 \ mathtt {+} e_2 \䞋向き矢印k}






「-」で「-」、「+」で「+」を定矩したのは少し奇劙に思えるかもしれたせん。 これは埪環䟝存ですか 答えはノヌです。 プラスずマむナスは、誰もが孊校で経隓する敎数の通垞の算術挔算です。 この意味で、Arithが32ビットたたは64ビットの算術挔算を䜿甚しないのはさらに奇劙です。 Arithを実装するプログラマは、パッケヌゞを䜿甚しおBigIntegerを操䜜し、算術を凊理できたす。



小さなステップのセマンティクス



操䜜セマンティクスの2番目の最も䞀般的なスタむルは、小さなステップのセマンティクスです。 このスタむルでは、態床は結果にプログラムを衚瀺したせん。 代わりに、プログラムを若干単玔化されたプログラムにマップしたす。このプログラムでは、郚分匏が結果に眮き換えられたす。 このスタむルはテキストの眮換ず考えるこずができたす。 このスタむルの䟋を挙げるには、Stepリレヌションを定矩したす。 この関係には、他の倚くの芁玠ず同様に、次の芁玠が含たれたす。 



 -2 + -5、--3∈ステップ
         --3、3∈ステップ


略語を再床玹介したす。 はe1、e2∈ステップを意味したす。 そしお、ステップをたずめるず、 意味する そしお 。 stepの同矩語は、reduceずいう甚語です。 前の2ステップの䟋は、次のように蚘述できたす。







次に、Stepを定矩するルヌルに進みたしょう。 以䞋で説明する5぀のルヌルがありたす。



\ begin {gather *}1\ frac {j = -i} {\ mathtt {-} i \ longrightarrow j} \ qquad2\ frac {k = i + j} {i \ mathtt {+} j \ longrightarrow k} \\ [3ex]3\ frac {e \ longrightarrow e '} {\ mathtt {-} e \ longrightarrow \ mathtt {-} e'} \ qquad4\ frac {e_1 \ longrightarrow e '_1} {e_1 \ mathtt {+} e_2 \ longrightarrow e'_1 \ mathtt {+} e_2} \ qquad5\ frac {e_2 \ longrightarrow e'_2} {i \ mathtt {+} e_2 \ longrightarrow i \ mathtt {+} e'_2} \ end {gather *}






ルヌル1ず2は最も興味深いものです。 圌らは算術を行いたす。 それらを「蚈算䞊の削枛ルヌル」ず呌びたす。 ルヌル3〜5を䜿甚するず、郚分匏に移動しお蚈算を実行できたす。 それらは、私たちが今に入っおこない理由でしばしば合同芏則ず呌ばれたす。 ルヌル5で倉数iを䜿甚するず、瞮小が巊から右に行われるこずを意味したす。 特に、巊の匏が敎数になるたで、右の匏を+蚘号から枛らすこずはできたせん。



䜙談ここで怜蚎しおいる巊から右の順序は、蚀語デザむナヌずしお遞択されおいたす。 順序を決定できず、あいたいになりたした。 私たちの蚀語には副䜜甚がないので、順序は関係ありたせん。 ただし、ほずんどの蚀語には副䜜甚があり、順序を決定したすすべおではありたせん。そのため、順序が通垞決定される方法の䟋を怜蚎する必芁があるず考えたした。



䟋の時間。 ステップの出力を芋おみたしょう。



3\ begin {array} {c}2\ begin {array} {c} \\\ hline \ mathtt {2 + -5} \; \ longrightarrow \; \ mathtt {-3} \ end {array} \\\ hline \ mathtt {-2 + -5} \; \ longrightarrow \; \ mathtt {--3} \ end {array}






蚈算の1ステップ、぀たり 関係ステップ。 しかし、ただ完了しおいたせん。 完了前にプログラムを実行するこずの意味をただ決定する必芁がありたす。 これを行うには、ステップ関係の芳点からEvalを定矩したす。 蚀い換えれば、匏eがれロ以䞊のステップで敎数iに還元される堎合、Eval '関係には任意のペアe、iが含たれたす。 以䞋に説明する新しい衚蚘法がありたす。







衚蚘{... ∣ ...}はセットコンストラクタを定矩したす。 垂盎バヌの巊偎の匏は、セットの兞型的な芁玠のテンプレヌトを定矩し、右偎の匏は、セットの芁玠の制限を定矩したす。 衚蚘法 れロ以䞊のステップを意味したす。 ルヌルを䜿甚しお、これらのマルチステップリレヌションシップを定矩したす。



\ frac {} {e \ longrightarrow ^ {*} e} \ qquad \ frac {e_1 \ longrightarrow e_2 \ quad e_2 \ longrightarrow ^ {*} e_3} {e_1 \ longrightarrow ^ {*} e_3}






私はLispのようなリストの芳点からそれに぀いお考える。だから、最初のルヌルはnilであり、2番目のルヌルはconsである。



型システム䟋ずしおラムダ蚈算を䜿甚



倚くのプログラミング蚀語は静的に型付けされおいたす。 コンパむラヌは、実際のコンパむルを実行する前にいく぀かの怜蚌チェックを実行したす。 通垞、チェック䞭に、コンパむラヌはオブゞェクトが適切に䜿甚されおいるこずを確認したす。 䟋えば、誰も敎数を関数ずしお䜿甚しようずしおいないずいうこずです。 蚀語蚭蚈者がどの特定のチェックを実行する必芁があるかを瀺す方法は、蚀語の型システムを定矩するこずです。 Arithは非垞に単玔なので、興味深い型チェックはありたせん。 TNLで繰り返し䜿甚されるより耇雑な蚀語-ラムダ蚈算技術的には、単玔化されたタむプのラムダ蚈算を怜蚎しおください。 ラムダ蚈算は、匿名関数のみで構成されたす。 ラムダ蚈算を拡匵しお、算術匏が含たれるようにしたす。 その埌、私たちの蚀語は次の文法によっお決定されたす。 



  e :: = i ∣ −e ∣ e + e ∣ x ∣ ee ∣λxTe


倉数xは、fooやgなどのパラメヌタヌ名をリストしたす。 右偎の次の2぀の匏eeは、関数の適甚たたは関数呌び出しを意味したす。 Cに粟通しおいる堎合、e1 e2をe1e2ず読むこずができたす。 ラムダ蚈算では、関数はパラメヌタヌを1぀だけ取るため、関数を呌び出すには1぀の匕数しか必芁ありたせん。 構文λxTeは、タむプTの1぀のパラメヌタヌxすぐにタむプを決定したすず匏eで構成される本䜓を持぀関数を䜜成したす。 倚くの堎合、xは関数の名前であるず誀解されたす。実際には、関数は匿名であるため、぀たり名前がないため、これはパラメヌタヌの名前です。関数の戻り倀は匏eの結果になりたす。 次に、プログラムの実行䞭にどのオブゞェクトが存圚するかを考えおみたしょう。 これらは敎数ず関数です。 Tを䜿甚しおさたざたなタむプを列挙し、さたざたなオブゞェクトを蚘述するために倚くのタむプを䜜成したす。







機胜タむプ 、T 1はパラメヌタヌのタむプ、T 2は戻り倀のタむプです。

型システムの仕事は、匏の結果が持぀倀の型を予枬するこずです。 たずえば、匏-5 + 2はInt型である必芁がありたす。これは、結果-5 + 2が数倀-3敎数であるためです。 蚀語の構文たたは操䜜䞊のセマンティクスを決定する堎合ず同様に、TNC理論家は関係ず芏則を䜿甚しお型システムを決定したす。 WellTypedリレヌションを定矩したす。これは、最初の近䌌では、匏を型にマッピングしたす。 たずえば、-5 + 2、Int∈WellTyped。

ただし、 ラムダ蚈算には倉数が含たれたす。どの倉数がどのタむプを持぀かを远跡するには、䜕らかの皮類のシンボルテヌブルアナログ、タむプ環境ず呌ばれる関係が必芁です。 ギリシャ文字のΓガンマは、この目的で䞀般的に䜿甚されたす。 倖郚スコヌプから倉数を隠す機胜を備えた、叀いものから新しいタむプの環境を䜜成できる必芁がありたす。 これらの可胜性の数孊的装眮を決定するために、xで始たるタプルが陀倖されるこずを陀き、Γ∖xはΓず同じ関係になるず仮定したす。 型システムの定矩方法によっおは、xで始たる0たたは1タプルがあり、型の環境を郚分関数ず呌ばれる特別な皮類の関係にする堎合がありたす。型環境を倉数xで拡匵し、堎合によっおは以前の定矩をオヌバヌラむドし、次のように定矩したす。



\ガンマ、x {} T =\ガンマ\バックスラッシュx\カップ\ {x、T\}






ず仮定する



\ Gamma_1 = \ {\ mathtt {foo}、\ mathtt {Int}、\ mathtt {g}、\ mathtt {Int} \ to \ mathtt {Int}\}






それから



\ begin {align *} \ Gamma_1、\ mathtt {g} {} \ mathtt {Int}= \ {\ mathtt {foo}、\ mathtt {Int}、\ mathtt {g}、\ mathtt { Int}\} \\ \ Gamma_1、\ mathtt {f} {}\ mathtt {Int} {\ to} \ mathtt {Int}{\ to} \ mathtt {Int}= \ {\ mathtt {foo}、\ mathtt {Int}、\ mathtt {g}、\ mathtt {Int} {\ to} \ mathtt {Int}、\ mathtt {f}、\ mathtt {Int} {\ to } \ mathtt {Int}{\ to} \ mathtt {Int}\} \ end {align *}






型環境は、コンパむラヌのグロヌバルシンボルテヌブルずは異なり、スコヌプごずに耇数の型環境がある堎合がありたす。 さらに、タむプ環境を曎新せず、代わりに、叀い環境ずわずかに異なる新しい環境を䜜成したす。 プログラミングの芳点から、ここで䜿甚する数孊的メタ蚀語は玔粋に機胜的です。 副䜜甚は含たれおいたせん。 読者はこれが非効率に぀ながるのではないかず心配するかもしれたせんが、ここでプログラムを曞いおいるのではなく、仕様を曞いおいるこずを思い出しおください 明快さは私たちにずっお最も重芁です。 そしお、枅朔に保぀こずで、より理解しやすいものを曞くこずができたす。

WellTypedリレヌションに戻るず、2぀の芁玠のタプル2タプル、ペアを含む代わりに、3぀の芁玠のタプル3タプル、トリプルの圢匏Γ、e、Tが含たれたす。 したがっお、型環境のコンテキストで型を匏に割り圓おたす。 もう1぀の略語を玹介したすTNL理論家は略語が倧奜きです。 曞きたす Γ、e、T∈WellTypedの代わりに。 これで、WellTypedを定矩するルヌルをリストする準備ができたした。



\ begin {gather *} \ frac {} {\ Gamma \ vdash i\ mathtt {Int}} \ qquad \ frac {\ Gamma \ vdash e\ mathtt {Int}} {\ Gamma \ vdash \ mathtt {-} e\ mathtt {Int}} \ qquad \ frac {\ Gamma \ vdash e_1\ mathtt {Int} \ quad \ Gamma \ vdash e_2\ mathtt {Int}} {\ Gamma \ vdash e_1 \ mathtt {+} e_2 \ mathtt {Int}} \\ [3ex] \ frac {x、T\ in \ Gamma} {\ Gamma \ vdash xT} \ qquad \ frac {\ Gamma、x {} T_1 \ vdash e T_2} {\ Gamma \ vdash\ lambda x {} T_1。ET_1 \ to T_2} \ qquad \ frac {\ Gamma \ vdash e_1T \ to T '\ quad \ Gamma \ vdash e_2 T} {\ Gamma \ vdash e_1 \、e_2T '} \ end {gather *}






䞊蚘のルヌルを芁玄したす。 算術挔算子は敎数で機胜したす。 倉数は環境からタむプを取埗したす。 ラムダは、パラメヌタヌのタむプず結果の出力タむプに基づいた機胜タむプです。 ラムダ本䜓は、このラムダのパラメヌタヌを䜿甚しお展開され、䜜成ポむントからの環境を䜿甚しおチェックされたす字句スコヌプ。 たた、関数の䜿甚は、匕数の型がパラメヌタヌの型ず䞀臎する限り、蚀語のロゞックに違反したせん。



おわりに



これで、プログラミング蚀語の理論で䜿甚されおいる衚蚘法でこのクラッシュコヌスが終了したす。 この投皿では基本のみを説明しおいたすが、必芁な远加の衚蚘法の倚くは、ここで説明した衚蚘法のバリ゚ヌションです。 お読みいただき、コメントで質問しおください。


More articles:


All Articles