Лямбда-числення: опис теореми, особливості, приклади

Для чайників

Лямбда-числення була введена математиком Алонзо Черчем в 1930-х роках в рамках дослідження основ науки. Первісна система була показана як логічно несумісна в 1935 році, коли Стівен Клин і Дж. Б. Россер розробили парадокс Кліні-Россера.

Надалі, у 1936 році Черч виділив і опублікував тільки ту частину, яка має відношення до розрахунків, те, що зараз називається нетипизированным лямбда-обчисленням. У 1940 він також представив більш слабку, але логічно несуперечливу теорію, відому як система простого типу. У свій роботі він пояснює всю теорію простою мовою, тому, можна сказати, що Черч опублікував лямбду обчислення для чайників.

До 1960-х років, коли з’ясувалося його ставлення до мов програмування, λ стала лише формалізмом. Завдяки застосуванням Річарда Монтегю та інших лінгвістів у семантиці природної мови, обчислення стало займати почесне місце як у лінгвістиці, так і в інформатиці.