2

したがって、次のタイプの式を見つけるように求められます。

(int -> ((int -> (bool -> int)) -> (bool -> int)))

だから私は（bool-> int）を生成するために次のコードを構築しましたしかしそれは私を悩ませている組み合わせです：

(%which (T)
        (%typing '(lambda (f)
                    (lambda (x)
                      (succ (f (not x)))))
                 T))

誰かが私に良いルールや方法を教えてもらえますか？:)

4

4 に答える 4

1

個人的には、型から冗長な括弧を削除すると、もう少し明白になると思います (非スキーマが書くように):

int -> (int -> bool -> int) -> bool -> int

したがって、3 つの引数が与えられ、 を返す関数を作成することになっていますint。つまり、解は次の形式で表現できなければなりません。

lambda n. lambda f. lambda b. ____

でもどうやって穴埋めするの？fパラメータから取得する型を見ると、 と に適用してnをb生成することで、それらを結合できることが簡単にわかりますint。そう：

lambda n. lambda f. lambda b. f n b

それが一つの解決策です。しかし、この項を注意深く見ると、最も内側のラムダが実際にはイータ簡約され、さらに単純な項になることがわかります。

lambda n. lambda f. f n

しかし実際には、int を返すことは常に些細なことなので、この質問は少し退化しています。したがって、おそらく最も簡単な解決策は次のとおりです。

lambda n. lambda f. lambda b. 0

解決策に到達するための一般的なスキームは、多くの場合、型構造の単純な誘導によるものです。関数が必要な場合は、ラムダを書き留めて、本体を再帰的に処理します。タプルが必要な場合は、タプルを書き留めて、そのコンポーネントを再帰的に処理します。プリミティブ型が必要な場合は、定数を選択するだけです。持っていないものが必要な場合 (通常はポリモーフィックの場合)、そのようなものを提供するスコープ内の関数パラメーターのいくつかを探します。そのパラメーター自体が関数である場合は、適切な引数を再帰的に構築してみてください。

于 2012-05-26T16:34:25.860 に答える
0

（一般的な手法ではなく）質問の詳細については、次のように説明します。

(int -> ((int -> (bool -> int)) -> (bool -> int)))(A -> ((A -> B) -> B))whereA = intとに簡略化できますB = (bool -> int)。この簡略化されたバージョンは簡単に作成できます。

(lambda (a)
  (lambda (f)
    (f a)))

これが機能する理由は簡単にわかります。hastypeaとAhastypefで(A -> B)あるため、呼び出す(f a)と。になりBます。これらの変数に具体的な型を置くにaは、型がありint、f型(int -> (bool -> int))があり、結果はもちろんです(bool -> int)。

(int -> (bool -> int))したがって、パラメータに挿入するタイプを持つ適切な関数を見つける必要がありfます。これは、次の例を作成するのは非常に簡単です。

(lambda (n)
  (lambda (negate?)
    ((if negate? - +) n)))

これらの関数の使用方法は次のとおりです。

> (define (foo a)
    (lambda (f)
      (f a)))
> (define (bar n)
    (lambda (negate?)
      ((if negate? - +) n)))
> (define baz ((foo 42) bar))
> (baz #t)
-42
> (baz #f)
42
于 2012-05-26T14:32:24.507 に答える
0

これは私が探した解決策です：

(ラムダ (i) (ラムダ (f) (ラムダ (b) (成功 ((f (成功 i)) (ない b))))))

(%which (T) (%typing '(lambda (i) (lambda (f) (lambda (b) (succ ((f (succ i)) (not b)))))) で確認できます。 T))

Succ は、それが整数であることを確認し、--> bool ではありません。

于 2012-05-27T08:36:28.407 に答える
0

型から実装を派生させるためのツールがいくつかあります (Curry/Howard 対応を介して)。例はDjinnです。一般に、型から用語を生成する方法を示す Introduction があります。

Curry-Howard についてもっと学び、型からコードへのツールを Scheme に移植できるかもしれません。

于 2012-05-26T13:26:47.640 に答える