Basis combinator tidak lengkap

Ini terinspirasi oleh pertanyaan ini . Misalkan adalah kumpulan semua kombinator yang hanya memiliki dua variabel terikat. Apakah lengkap secara kombinasi? $\mathcal{C}$ $\mathcal{C}$

Saya percaya jawabannya negatif, namun saya tidak dapat menemukan referensi untuk ini. Saya juga akan tertarik pada referensi untuk bukti ketidaklengkapan kombinatorial dari set combinator (saya dapat melihat mengapa set terdiri dari combinator dengan hanya satu variabel terikat tidak lengkap, sehingga set ini harus mengandung lebih dari sekedar elemen ). $\mathcal{D}$ $\mathcal{D}$

lo.logic lambda-calculus combinatory-logic tci
sumber

Bisakah Anda mengklarifikasi apa yang Anda maksud dengan jumlah variabel terikat dari combinator (= istilah lambda tertutup)? Total jumlah abstraksi lambda?

Noam Zeilberger

Ya, ini yang saya maksud.

tci

Sebenarnya, mungkin bukan itu yang Anda maksudkan ... mungkin yang Anda maksud adalah jumlah total variabel berbeda yang digunakan dalam abstraksi lambda, jadi misalnya

memiliki dua variabel terikat yang berbeda, meskipun memiliki empat abstraksi lambda? Dalam hal ini, tampaknya Rick Statman menjawab pertanyaan ini (negatif), dalam " Dua variabel tidak cukup ".

(λ x . x (λ y . y)) (λ x . λ y . x y)

$(\lambda x.x(\lambda y.y))(\lambda x.\lambda y.x y)$

Noam Zeilberger

Baik. Saya pikir ini adalah jawaban yang saya cari, dan saya pasti berharap itu adalah hasil dari Statman. Saya belum memeriksa, tapi saya pikir ini juga akan memberikan jawaban negatif untuk pertanyaan yang saya sebutkan. Jika Anda mempostingnya sebagai jawaban, saya dengan senang hati akan menerimanya.

tci

Jawaban:

[Memperluas komentar menjadi jawaban.]

$t$

the total number of distinct bound variable names in t

$\text{the total number of distinct bound variable names in }t$

t = (λ x . x (λ y . y)) (λ x . λ y . y x)

$t = (\lambda x.x(\lambda y.y))(\lambda x.\lambda y.yx)$

α

$\alpha$

t

$t$

α

$\alpha$

t^{'} = (λ x . x (λ y . y)) (λ a . λ b . b a)

$t' = (\lambda x.x(\lambda y.y))(\lambda a.\lambda b.ba)$

t^{'}

$t'$

t

$t$

the maximum number of free variables in a subterm of t

$\text{the maximum number of free variables in a subterm of }t$

α

$\alpha$

$\mathcal{C}$

Tampaknya bukti asli dari ini terkandung dalam laporan teknologi oleh Rick Statman:

Combinators dengan Hereditarily dari Order Two. Laporan Teknis Departemen Matematika Carnegie Mellon 88-33, Agustus 1988. ( pdf )

$\beta$

Dua variabel tidak cukup. Prosiding konferensi ke-9 Italia tentang Theoretical Computer Science, hal. 406-409, 2005. ( acm )

$Hn$ $Hn$ $n+1$ $\beta$ $n$ $S = \lambda x.\lambda y.\lambda z.(xz)(yz)$ $n$ $n$ $Hn$ $n+1$

Noam Zeilberger
sumber