Dapatkah aljabar boolean diekspresikan dalam lambda caclulus yang diketik sederhana?

15

Aljabar Boolean dapat diekspresikan dalam kalkulus lambda yang tidak diketik dalam (misalnya) dengan cara ini.

true  = \t. \f. t;
false = \t. \f. t;
not   = \x. x false true;
and   = \x. \y. x y false;
or    = \x. \y. x true y;

Aljabar boolean juga dapat dikodekan dalam Sistem F dengan cara ini :

CBool = All X.X -> X -> X;
true  = \X. \t:X. \f:X. t;
false = \X. \t:X. \f:X. f;
not   = \x:CBool. x [CBool] false true;
and   = \x:CBool. \y:CBool. x [CBool] y false;
or    = \x:CBool. \y:CBool. x [CBool] true y;

Apakah ada cara untuk mengekspresikan aljabar boolean dalam kalkulus lambda yang diketik sederhana? Saya berasumsi bahwa jawabannya adalah TIDAK. ( Misalnya, Pendahuluan dan daftar tidak dapat diwakili dalam kalkulus lambda yang diketik sederhana .) Jika jawabannya memang TIDAK, apakah ada penjelasan intuitif sederhana, mengapa tidak mungkin untuk menyandikan boolean di kalkulus lambda yang diketik sederhana?

PEMBARUAN: Kami berasumsi bahwa ada tipe dasar.

UPDATE: Jawaban negatif dengan penjelasan ditemukan di sini (Komentar "Di sini adalah sketsa bukti untuk menunjukkan bahwa kalkulus lambda yang diketik dengan produk dan banyak tipe dasar yang tidak memiliki boolean.") Inilah yang saya cari.

lo.logic type-theory lambda-calculus Ilya Klyuchnikov
sumber
2
Coba ketikkan definisi ke Haskell dan lihat apa yang terjadi ketika Anda memberikan tipe pada berbagai ekspresi. Anda akan melihat bahwa kode sangat bergantung pada polimorfisme.
Dave Clarke
2
Maaf menjadi pedantic, tetapi pertanyaan tentang ekspresifitas kalkulus ini atau itu menjadi bermakna hanya dengan pemahaman yang jelas tentang apa yang Anda maksud dengan "diekspresikan", "disandikan" dan "diwakili", karena ada beberapa cara yang masuk akal untuk memahami istilah-istilah ini. Selain itu, karena Anda menentukan keberadaan tipe dasar, Anda harus spesifik tentang apa itu, dan konstruktor / penghancur apa yang mereka miliki.
Martin Berger
3
Maaf saya tidak bertele-tele. Jawabannya ditemukan di sini: math.andrej.com/2009/03/21/…
Ilya Klyuchnikov
3
Saya merasa seperti saya harus mendapatkan kredit untuk menjalankan blog yang bagus :-)
Andrej Bauer
7
Definisi tipe Boolean yang digunakan di blog lebih kuat daripada di sini. Faktanya, jawaban Jeremy menunjukkan bahwa cukup mengetik kalkulus lambda dengan setidaknya satu tipe dasar (sebut saja ) dapat mengekspresikan aljabar Boolean dalam arti OP: define B = O → O → O , t r u e = λ x : O . λ y : O . x , f suatu l s e = λ x : O . λ y :OB=O→O→Otrue=λx:O.λy:O.x , n o t = λ a : B . λ x : O . λ y : O . a y x , a n d = λ a : B . λ b : B . λ x : O . λ y : O . a ( b x y ) y , o rfalse=λx:O.λy:O.ynot=λa:B.λx:O.λy:O.ayxand=λa:B.λb:B.λx:O.λy:O.a(bxy)y . or=λa:B.λb:B.λx:O.λy:O.ax(bxy)
Emil Jeřábek mendukung Monica

Jawaban: