Jaki był pierwotny zamiar stworzenia rachunku Lambda?

22

Czytałem, że początkowo Kościół zaproponował -calculus jako część swoich postulatów z logiki (co jest gęstym odczytem). Ale Kleene udowodnił, że jego „system” jest niespójny, po czym Church wyodrębnił odpowiednie rzeczy do swojej pracy nad „skutecznym obliczeniem” i porzucił wcześniejsze prace nad logiką. $\lambda$

Tak jak ja rozumiem, -system i jego oznaczenia wziął formę jako część czegoś wspólnego z logiką. Co Kościół początkowo starał się osiągnąć, aby później rozwidlił się? Jakie były początkowe powody utworzenia -calculus? $\lambda$ $\lambda$

— Doktorat
źródło

1

Literówka w tytule ...

— user11153

26

Chciał stworzyć formalny system dla podstaw logiki i matematyki, który byłby prostszy niż teoria typów Russella i teoria mnogości Zermelo.

Podstawową ideą było dodanie stałej do nietypowego rachunku lambda (lub logiki kombinacyjnej) i interpretacja jako wyrażenia „ spełnia predykat ”, a jako wyrażenia „ ”. Z regułami wyrażającymi te intencje można interpretować fragment intuicyjnej logiki predykatów i nieograniczonego zrozumienia, jedynym problemem jest to, że w paradoksie Curry'ego każdy można wyprowadzić. $\Xi$ $XZ$ $Z$ $X$ $\Xi XY$ $X\subseteq Y$ ${\to}{\forall}$ $X$

Patrz str. 7 z:

Cardone i Hindley, Historia rachunku Lambda i logiki kombinatorycznej , 2006: http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf

Jak również wprowadzenie do:

Barendregt, Bunder i Dekkers, Układy logiki kombinatoryjnej kompletne dla rachunku zdań i predykatów pierwszego rzędu , JSL 58-3 (1993): http://ftp.cs.ru.nl/CompMath.Found/ICL1.ps

— Ulrik Buchholtz
źródło

8

„Jedynym problemem jest to, że według paradoksu Curry'ego każdy można uzyskać” :) Warto przypomnieć, jaki jest paradoks Curry'ego : Biorąc pod uwagę, że istnieje termin taki, że dla każdego , wówczas można napisz który jest twierdzeniem takim, że , podając taką samą sprzeczność jak w paradoksie Russela. Nieterminacja jest tutaj kluczowa, co zmotywowało stworzenie po prostu wpisanego -calculus, w którym każdy termin się kończy.

X

$X$

Y

$Y$

Y M = M (Y M)

$YM=M(YM)$

M

$M$

Y (\neg)

$Y(\neg)$

ϕ

$\phi$

ϕ \Leftrightarrow \neg ϕ

$\phi\Leftrightarrow\neg\phi$

λ

$\lambda$

— cody

2

Nie jestem pewien, czy była to część motywacji do utworzenia rachunku lambda, ale rachunek lambda został wykorzystany do rozwiązania problemu Entscheidungsproblem , postawionego przez Hilberta w 1928 roku. Turing samodzielnie rozwiązał problem Entscheidungsproblem poprzez wprowadzenie maszyny Turinga.

Z artykułu w Wikipedii na temat Entscheidungsproblem:

W 1936 r. Alonzo Church i Alan Turing opublikowali niezależne artykuły [2] wykazujące, że ogólne rozwiązanie Entscheidungsproblem jest niemożliwe, zakładając, że intuicyjne pojęcie „skutecznie obliczalnego” jest uchwycone przez funkcje obliczalne przez maszynę Turinga (lub równoważnie przez wyrażalne w rachunku lambda).

— littleO
źródło

1

To jest „następstwo” wcześniejszego rachunku Lambda. Właśnie wykorzystał jego krytyczną część, aby podać definicję efektywnej kalkulacji.

— Doktorat