8

stack固定小数点コンビネータを使用して、ラムダ計算でデータ構造を定義しようとしています。2つの操作、insertionおよびremoval要素のso、pushおよびを定義しようとしてpopいますが、定義できた唯一の操作である挿入が正しく機能していません。削除の定義方法がわかりませんでした。

これが私の操作に対するアプローチであり、 ：pushの定義です。stack

Stack definition:
STACK = \y.\x.(x y)
PUSH = \s.\e.(s e)

私のスタックは、一番下を示す要素で初期化されています。私は0ここを使用しています：

stack = STACK 0 = \y.\x.(x y) 0 = \x.(x 0)       // Initialization
stack = PUSH stack 1 = \s.\e.(s e) stack 1 =     // Insertion
    = \e.(stack e) 1 = stack 1 = \x.(x 0) 1 =
    = (1 0)

しかし、今、別の要素を挿入しようとすると、初期構造が分解されているため、機能しません。

STACK定義または定義を修正するにはどうすればよいですか？また、操作PUSHを定義するにはどうすればよいですか？POP再帰を許可するには、コンビネータを適用する必要があると思いますが、その方法がわかりませんでした。

参照： http： //en.wikipedia.org/wiki/Combinatory_logic

ラムダ計算でのデータ構造の定義に関する詳細な説明や例をいただければ幸いです。

4

2 に答える 2

11

コンビネータを定義することにより、次のようになります。

は自由変数のないラムダ項として定義されているため、定義上、任意のコンビネータはすでにラムダ項です。

たとえば、次のように記述して、リスト構造を定義できます。

Y = (list definition in lambda calculus)
Y LIST = (list definition in lambda calculus) LIST
Y LIST = (element insertion definition in lambda calculus)

直感的に、そして不動点コンビネータを使用して、可能な定義は次のとおりです-\ =lambdaを考慮してください：

  • リストは空で、その後に末尾の要素が続きます0。
  • または、リストは要素によって形成されxます。これは、前のリスト内の別のリストである可能性があります。

コンビネータ（固定小数点コンビネータ）で定義されているため、さらにアプリケーションを実行する必要はありません。次の抽象化は、ラムダ用語そのものです。

Y = \f.\y.\x.f (x y)

今、それをリストと名付けます：

Y LIST = (*\f*.\y.\x.*f* (x y)) *LIST* -- applying function name
LIST = \y.\x.LIST (x y), and adding the trailing element "0"
LIST = (\y.\x.LIST (x y) ) 0
LIST = (*\y*.\x.LIST (x *y*) ) *0*
LIST = \x.LIST (x 0), which defines the element insertion abstraction.

固定小数点コンビネータY、または単にコンビネータを使用すると、自由変数がないため、削減の必要がなく、LISTの定義がすでに有効なメンバーであると見なすことができます。

次に、次のようにして、要素、たとえば1と2を追加/挿入できます。

LIST = (\x.LIST (x 0)) 1 2 =
    = (*\x*.LIST (*x* 0)) *1* 2 =
    = (LIST (1 0)) 2 =

しかし、ここでは、リストの定義を知っているので、それを拡張します。

    = (LIST (1 0)) 2 =
    = ((\y.\x.LIST (x y)) (1 0)) 2 =
    = ((*\y*.\x.LIST (x *y*)) *(1 0)*) 2 =
    = ( \x.LIST (x (1 0)) ) 2 =

ここで、elemenetを挿入します2。

    = ( \x.LIST (x (1 0)) ) 2 =
    = ( *\x*.LIST (*x* (1 0)) ) *2* =
    = LIST (2 (1 0))

LISTはコンビネータで定義されたラムダ項であるため、新しい挿入の場合は拡張することも、そのままにしておくこともできます。

将来の挿入のために拡張：

    = LIST (2 (1 0)) =
    = (\y.\x.LIST (x y)) (2 (1 0)) =
    = (*\y*.\x.LIST (x *y*)) *(2 (1 0))* =
    = \x.LIST (x (2 (1 0))) =
    = ( \x.LIST (x (2 (1 0))) ) (new elements...)

これを自分で導き出すことができて本当にうれしいですが、スタック、ヒープ、またはより洗練された構造を定義するときは、いくつかの追加の条件が必要であると確信しています。

スタックの挿入/削除の抽象化を導き出そうとしています-すべてのステップバイステップなしで：

Y = \f.\y.\x.f (x y)
Y STACK 0 = \x.STACK (x 0)
STACK = \x.STACK (x 0)

その上で操作を実行するために、空のスタックに名前を付けましょう-変数を割り当てます（：

stack = \x.STACK (x 0)

// Insertion -- PUSH STACK VALUE -> STACK
PUSH = \s.\v.(s v)
stack = PUSH stack 1 =
    = ( \s.\v.(s v) ) stack 1 =
    = ( \v.(stack v) ) 1 =
    = ( stack 1 ) = we already know the steps from here, which will give us:
    = \x.STACK (x (1 0))

stack = PUSH stack 2 =
    = ( \s.\v.(s v) ) stack 2 =
    = ( stack 2 ) =
    = \x.STACK x (2 (1 0))

stack = PUSH stack 3 =
    = ( \s.\v.(s v) ) stack 3 =
    = ( stack 3 ) =
    = \x.STACK x (3 (2 (1 0)))

そして、もう一度、この結果に名前を付けて、要素をポップします。

stack = \x.STACK x (3 (2 (1 0)))

// Removal -- POP STACK -> STACK
POP = \s.(\y.s (y (\t.\b.b)))
stack = POP stack =
    = ( \s.(\y.s y (\t.\b.b)) ) stack =
    = \y.(stack (y (\t.\b.b))) = but we know the exact expansion of "stack", so:
    = \y.((\x.STACK x (3 (2 (1 0))) ) (y (\t.\b.b))) =
    = \y.STACK y (\t.\b.b) (3 (2 (1 0))) = no problem if we rename y to x (:
    = \x.STACK x (\t.\b.b) (3 (2 (1 0))) =
    = \x.STACK x (\t.\b.b) (3 (2 (1 0))) = someone guide me here, if i'm wrong
    = \x.STACK x (\b.b) (2 (1 0)) =
    = \x.STACK x (2) (1 0) =
    = \x.STACK x (2 (1 0))

うまくいけば、要素3がポップされます。

私はこれを自分で導き出そうとしたので、私が従わなかったラムダ計算からの制限がある場合は、それを指摘してください。

于 2012-12-03T08:59:34.107 に答える
8

ラムダ計算のスタックは、単一リンクリストにすぎません。また、単一リンクリストには2つの形式があります。

nil  = λz. λf. z
cons = λh. λt. λz. λf. f h (t z f)

これはチャーチエンコーディングであり、リストはそのカタモルフィズムとして表されます。重要なのは、固定小数点コンビネータはまったく必要ないということです。nilこのビューでは、スタック（またはリスト）は、ケースに対して1つの引数を取り、ケースに対して1つの引数を取る関数consです。たとえば、リスト[a,b,c]は次のように表されます。

cons a (cons b (cons c nil))

空のスタックは、SKI計算nilのコンビネータに相当します。コンストラクターはあなたのK操作です。ヘッド要素とテール用の別のスタックが与えられると、結果は、要素が前面にある新しいスタックになります。conspushhth

このpop操作では、リストを頭と尾に分解するだけです。これは、2つの関数を使用して実行できます。

head = λs. λe. s e (λh. λr. h)
tail = λs. λe. s e (λh. λr. r nil cons)

e空のスタックのポップは定義されていないため、空のスタックを処理するものはどこにありますか。headこれらは、とのペアを返す1つの関数に簡単に変換できますtail。

pop = λs. λe. s e (λh. λr. λf. f h (r nil cons))

この場合も、ペアはチャーチ数でエンコードされています。ペアは単なる高階関数です。このペア(a, b)は、高階関数として表されますλf. f a b。これは、別の関数が与えられた場合に、との両方にf適用される単なる関数です。fab

于 2012-12-27T02:58:22.443 に答える