Loogika aine ja ajalugu
väidete tuletuste leidmiseks sageli rohkem aega kuluda kui universumil vanust.
1936. aastal esitas Alonzo Church minimaalsete vahenditega algoritmikirjutamise- ehk progammeerimiskeele, nn.
lambda-arvutuse. Lambda-arvutus erineb kardinaalselt Turingi masinast, kuid teoreetiliselt on neil samasugused
arvutamisvõimed: üks on teises algoritmiliselt simuleeritav. Churchi loodud lambda-arvutus on kaasaegsete
funktsionaalsete programmeerimiskeelte eellane, ning tema teoreetiline tähtsus praegusagses loogikas ja teoreetilises
arvutiteaduses on erinevalt Turingi masinast väga suur. Analoogiliselt Turingile tõestas Church, et lambda-arvutuse
abstraktse masina abil ei ole võimalik alati otsustada, kas suvaline formaalse aritmeetika teoreem on formaalse
aritmeetika reeglitest tuletatav või mitte.
Churchi nime mainitakse kõige sagedamini seoses nn. Churchi teesiga. Nimelt väitis Church, et ükskõik millise
algoritmi saab esitada lambda-arvutuse abil