18

私は SICP を使って作業していますが、問題 2.6によって私は困惑しています。チャーチ数を扱う場合、0 と 1 を特定の公理を満たす任意の関数にエンコードするという概念は理にかなっているように思われます。さらに、ゼロの定義と add-1 関数を使用して個々の数を直接定式化することは理にかなっています。プラス演算子を形成する方法がわかりません。

これまでのところ、私はこれを持っています。

(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))

lambda calculusのウィキペディアのエントリを調べたところ、 plus の定義は PLUS := λmnfx.mf (nfx) であることがわかりました。その定義を使用して、次の手順を定式化することができました。

(define (plus n m)
  (lambda (f) (lambda (x) ((m f) ((n f) x)))))

私が理解していないのは、以前に派生したプロシージャによって提供された情報のみを使用して、そのプロシージャを直接派生させる方法です。厳密な証明のような形式でこれに答えることができる人はいますか? 直感的には何が起こっているのか理解できると思いますが、Richard Feynman がかつて言ったように、「構築できなければ、理解することはできません...」

4

3 に答える 3

14

それは実際には非常に簡単です。これはおそらく火あぶりと見なされるでしょうが、括弧があるとわかりにくくなります。何が起こるかを理解するより良い方法は、カリー化された言語を使用していると想像するか、Scheme には多引数関数があり、それを受け入れてください...便利な場所でラムダと複数の引数を使用する説明を次に示します。

  • すべての数値 N は次のようにエンコードされます。

    (lambda (f x) ...apply (f (f (f ... (f x)))) N times...)

  • これは、N のエンコーディングが実際には

    (lambda (f x) (f^N x))

    どこf^Nで関数べき乗です。

  • これをより簡単に言うと (カリー化を想定): 数値 N は次のようにエンコードされます。

    (lambda (f) f^N)

    したがって、N は実際には「N 乗」関数です。

  • ここで式を考えてみましょう (ここで s の中を見てlambdaください):

    ((m f) ((n f) x))

    nis は数値のエンコードであるため、そのべき乗であるため、これは実際には次のようになります。

    ((m f) (f^n x))

    と同じm：

    (f^m (f^n x))

    残りは明らかなはずです...適用された適用されたmの適用されたの適用があります。fnfx

  • 最後に、楽しみを残すために、を定義する別の方法を次に示しますplus。

    (define plus (lambda (m) (lambda (n) ((m add1) n))))

    (まあ、これはおそらくもっと明白なので、あまり楽しいことではありません。)

于 2010-10-12T07:53:34.253 に答える
3

(高階関数を理解していることを確認してください) . Alonzo Churchの型なしラムダ計算では、関数が唯一のプリミティブ データ型です。数値、ブール値、リストなどはなく、関数のみです。関数は引数を 1 つしか持つことができませんが、関数は関数を受け入れたり返したりすることができます。これらの関数の値ではなく、関数自体です。したがって、数値、ブール値、リスト、およびその他のタイプのデータを表すには、無名関数がそれらを表す賢い方法を考え出す必要があります。チャーチナンバーは、自然数を表す方法。型指定されていないラムダ計算の 3 つの最も基本的な構造は次のとおりです。

  1. λx.x恒等関数は、何らかの関数を受け取り、すぐにそれを返します。
  2. λx.x x、自己申請。
  3. λf.λx.f x、関数適用、関数と引数を取り、関数を引数に適用します。

0、1、2 を関数以外の何物でもないものとしてどのようにエンコードしますか? どういうわけか、量の​​概念をシステムに組み込む必要があります。関数のみがあり、すべての関数は 1 つの引数にのみ適用できます。量に似たものはどこに見られますか? 関数をパラメーターに複数回適用できます。関数の 3 回の呼び出しの繰り返しには明らかに量感がありますf (f (f x))。それでは、ラムダ計算でエンコードしましょう。

  • 0 =λf.λx.x
  • 1 =λf.λx.f x
  • 2 =λf.λx.f (f x)
  • 3 =λf.λx.f (f (f x))

等々。しかし、0 から 1、または 1 から 2 になるにはどうすればよいでしょうか。数値を指定すると、1 ずつインクリメントされた数値を返す関数をどのように記述しますか? 用語が常に f で始まり、 fλf.λx.の有限の繰り返し適用があるという教会数字のパターンが見られるため、何らかの方法で の本体に入り、別の にラップする必要があります。縮小せずに抽象化の本体をどのように変更しますか? 関数を適用し、本体を関数でラップしてから、新しい本体を古いラムダ抽象化にラップできます。しかし、引数を変更したくないので、同じ名前の値に抽象化を適用します: 、ただし、これは必要なものではありません。λf.λx.f((λf.λx.f x) f) x → f x((λf.λx.f x) a) b) → a b

そのため、add1にλn.λf.λx.f ((n f) x)適用nしfてxから式をボディに還元し、fそのボディに適用してから、 で再び抽象化しλf.λx.ます。演習:それが本当であることを確認するには、すぐにβ 還元(λn.λf.λx.f ((n f) x)) (λf.λx.f (f x))を学び、 2 を 1 ずつ増やすように還元します。

本体を別の関数呼び出しにラップすることの背後にある直感を理解したところで、2 つの数値の加算をどのように実装するのでしょうか? λf.λx.f (f x)(2) とλf.λx.f (f (f x))(3) を指定すると (5) を返す関数が必要λf.λx.f (f (f (f (f x))))です。2 を見てください。それを 3 の本体に置き換えることができたらどうでしょうか。3 のボディを取得するには、それを適用してから. ここで 2 をに適用しますが、それを ではなく 3 の本体に適用します。次に、もう一度ラップします。xf (f (f x))fxfxλf.λx.λa.λb.λf.λx.a f (b f x)

結論:a 2 つの数字を加算するbには、両方とも教会の数字として表されます。 inを の本体に置き換え て、+ = . これを実現するには、 に適用し、次に に適用します。xabf (f x)f (f (f x))f (f (f (f (f x))))afb f x

于 2014-12-26T19:29:34.533 に答える
2

Eli の答えは技術的には正しいですが、この質問がされた時点では#apply手順が導入されていないため、著者が学生にその知識や、これに答えることができるカレーなどの概念の知識を持たせることを意図しているとは思いません。質問。

彼らは、置換法を適用することを提案することで、ほとんど答えに導きます。そして、そこから、加算の効果は、ある数値が別の数値に合成されることに気付くはずです。構成は演習 1.42 で導入された概念です。このシステムで付加的な手順がどのように機能するかを理解するために必要なことはこれだけです。

; The effect of procedure #add-1 on `one`, and `two` was the composition of `f` 
; onto `one` and `f` onto `two`.
;
; one   : (λ (f) (λ (x) (f x)))
; two   : (λ (f) (λ (x) (f (f x))))
; three : (λ (f) (λ (x) (f (f (f x)))))
;
; Thus one may surmise from this that an additive procedure in this system would
; work by composing one number onto the other.
;
; From exercise 1.42 you should already have a procedure called #compose.
;
; With a little trial and error (or just plain be able to see it) you get the
; following solution.

(define (adder n m)
  (λ (f)
    (let ((nf (n f))
          (mf (m f)))
      (compose nf mf))))
于 2014-05-12T23:52:10.100 に答える