Lambda Calculus-情報の定理

2049 ワード
プログラミング言語論 テキストリンク
https://jurogrammer.tistory.com/133?category=959000を学習し、作成を参照します.

Lambda Calculus

  • 形式システムで、計算の数学論理を表す.
  • 機能の抽象形式.
  • 変数を接続/置換することによって、関数に適用します.

    • Notation

  • lambda演算における有効マーキング法

    • Lambda terms


  • Value:変数.パラメータまたは数学、論理値.(数学:1,2,3/論理学:真,偽)
  • 抽象:関数を定義します.
  • (λx.M)記号:関数(λ)を選択し、xを挿入するとM(または置換、変換)を返します.
    (ex)f(x)=x^2+2を抽象記号として?->xはfx(x)のxに相当する.Mはx^2+2に相当する.
  • Application
  • 関数にLambdaを挿入します.
    (ex)f(x)=x^2+2に2->(λx.x^2+2) (2) 
    • # x=2 대입
function (x):
	return x^2+2
  • lambda演算に変数宣言X->が存在するλx.x+y:input入力x,xに未知のy,
    • を加える

    Operation



    1. α-conversion

  • は変数名のみを変更します.同じ意味
  • f(x)=x^2+2で表し、f(t)=t^2+2で表しますが、関数の動作方式に差はありません.
  • λx.x^2+2のxとλx.x+2のxは異なるxであり,操作時に混同する可能性がある.したがって,name競合を回避するために別の変数(α-conversion)

    • 2. β-reduction


    簡単に言えば、f(x)=x^2+2関数に2を代入する式f(2)=2^2+2β-還元と呼ぶ.
  • ((λx.M)E)このように書くと(M[x:=E])となります.すなわち,MにEを加えたのは
    • である.
  • (λx.x^2+2という2つのlambda項λx.x^2+2[x:=2]または6はlambda項に減少した.(β-reduction)
  • その他の注意事項

    • Free variables

  • λx.x^2+2->xはx^2+2バインドに関するものといえる.これに対してfree変数も存在する.
  • Free変数の定義
    変数xのみを見るとx自体がfree変数
  • λx.tのfree変数セットは、tのfree変数セットである.ただしxは
    • を除く
  • tsの自由変数セットは、tの自由変数セットとsの自由変数セットの合計である.
    • ex 1) λx.x
    1. λx.xでは、右側のxは1を定義するfree変数です.
    2.lambda用語λx.xを確認します.2番が適用されている場合、tに対応するxのfree変数はxであり、左側ramdaの隣の変数xは除外される.したがって,{x}-{x}にはfree変数はありません!そう言ってもいいです.
    ex 2) λx.yx
    ->yはfree変数

    Capture-avoiding substitutions

  • を置換して、同じ意味の取得を回避します(α-変換関連)

    • brancket(カッコ)の使用

    • を使用してぼかしを除去

    functions that operate on functions

  • lambda演算では、関数は1級値とみなされる.したがって、関数は入力でも出力でもよい.
    • 関数ポインタ
    4週間に2回(RGB距離)