ラムダ計算のリスト要素の合計とリストの長さ

Question

ラムダ計算のリスト要素の合計とリストの長さを計算するための関数を作成しようとしています。リストの
例：a := [1, 2, 3] = λcn.c 1 (c 2 (c 3 n))
sum a 6を返す必要がありますし、len a私は再帰的なバージョンを書いた3

返す必要があります：

、空、プラス、テールは他のラムダ関数であれば

len = λl.if (empty l) 0 (plus 1 (len (tail l))) 
sum = λl.if (empty l) 0 (plus (head l) (sum (tail l))) 

。

len = λl.if (empty l) 0 (plus 1 (len (tail l))) 
len = λfl.if (empty l) 0 (plus 1 (f (tail l))) len 
len = Y λfl.if (empty l) 0 (plus 1 (f (tail l))) 

Y = λf.(λx.f(x x))(λx.f(x x))
合計のためだけに同じ：

は、それから私は、不動点コンビネータといくつかのトリックをしました。だから私は非再帰的なバージョンがあります。しかし、ベータ版を使用してベータ版を得ることはできません。
これらの関数のベータ正規形がどのように見えるのだろうかと思います。

Answer 1

これらは、はるかに容易リストは、独自の反復子によってコードされていることを考えると実現することができる。

a := [1, 2, 3] = λcn.c 1 (c 2 (c 3 n)) 

リストは、2つの引数の関数であることを意味一consノードで使用するための一つの最後にnilコンストラクタで使用してください。

• がconsノードに格納された値を無視して、+1
• がに変換0

でnilを置き換える返す：

あなたが言って lengthを実装することができます結果として

length := λl. l (λ_. plus 1) 0 

拡大する

（それぞれで太字の式が折り畳まれていないか、減少のいずれかであることされている行）：

• 値を組み合わせること+を使用します。
  同様

  length a 
  (λl. l (λ_. plus 1) 0) a 
  (λl. l (λ_. plus 1) 0) (λcn.c 1 (c 2 (c 3 n))) 
  (λcn. c 1 (c 2 (c 3 n))) (λ_. plus 1) 0 
  (λn. (λ_. plus 1) 1 ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))) 0 
  (λ_. plus 1) 1 ((λ_. plus 1) 2 ((λ_. plus 1) 3 0)) 
  (plus 1) ((λ_. plus 1) 2 ((λ_. plus 1) 3 0)) 
  (plus 1) ((plus 1) ((λ_. plus 1) 3 0)) 
  (plus 1) ((plus 1) ((plus 1) 0)) 
  (plus 1) ((plus 1) 1) 
  (plus 1) 2 
  = 3

  、あなたが言ってsumを実装することができますconsに保存されているとテール

• の評価結果は、0

で nilを置き換えます変換

：あなたは '1'を言うときので

sum a 
(λl. l plus 0) a 
(λl. l plus 0) (λcn.c 1 (c 2 (c 3 n))) 
(λcn. c 1 (c 2 (c 3 n))) plus 0 
(λn. plus 1 (plus 2 (plus 3 n))) 0 
plus 1 (plus 2 (plus 3 0)) 
plus 1 (plus 2 3) 
plus 1 5 
= 6