Алонзо Черч: відмінності між версіями

[неперевірена версія][неперевірена версія]
Вилучено вміст Додано вміст
Немає опису редагування
мНемає опису редагування
Рядок 6:
* У [[1932]] році з метою мінімізації кількості логічних операторів ввів спеціальний лямбда-оператор або ж оператор абстракції, який дозволяв по будь-якому функціональному виразу побудувати назву відповідної функції. На основі двох логічних операторів: аплікації (застосування функції до аргументу) та абстракції — збудував т. зв. [[Лямбда-числення|лямбда-числення]], яке мало прислужитися для серйозного дослідження основ математики. Від цих планів довелося відмовитися, оскільки [[Клейні Стефен Коул|С. К. Клейні]] довів, що лямбда-числення суперечливе. Подальші розробки теорії оператора лямбда належать [[Каррі Хаскел|Х. Каррі]]. Попри суперечливість, лямбда-числення знайшло практичне застосування, полягши в основу [[функціональне програмування|функціональних мов програмування]], зокрема родини [[Лісп]] (наприклад, [[Scheme]]).
 
* У [[1935]] році (опубліковано в наступному 1936 році) ЧорчЧерч збудував перший приклад нерозв'язної масової проблеми. Цей приклад доводив існування проблем, які в принципі неможливо розв'язати. На основі цього відкриття у 1935-36 роках зусиллями [[Пост Еміль|Е. Поста]], [[Клейні Стефен Коул|С. К. Клейні]], [[ТьюрінгАлан АланТюрінг|А.Алана ТьюрінгаТюрінга]] і самого Черча була збудована теорія обчислюваності (або розв'язності), яка нині посідає помітне місце в корпусі всієї математики. Черчу належить уточнення поняття обчислюваної функції у вигляді лямбда-означуваної функції.
 
* Видатним науковим результатом Черча було опубліковане в [[1936]] році доведення теореми про нерозв'язність першопорядкового числення предикатів. Ця теорема, яка говорить про неможливість механічного обчислення істини, носить назву [[Теорема Черча|теореми Черча]].