Ля́мбда-абстра́кция Чёрча, способ введения функций в языках математической логики, в особенности в комбинаторной логике. А именно: если в некотором точном языке определён терм $A$, выражающий объект теории и зависящий от параметров $x_1, \ldots, x_n$ (и, может быть, также от других параметров), то$$\tag{*}\lambda x_1 \ldots x_n A$$служит в языке обозначением функции, перерабатывающей значения аргументов $x_1, \ldots, x_n$ в объект, выражаемый термом $A$. Выражение (*) и называется $\lambda$-абстракция Чёрча. Эта $\lambda$-абстракция Чёрча, называемая также явным определением функций, употребляется чаще всего в случае, когда в языке теории возникает опасность смешения функции как объекта исследования со значениями функции для некоторых значений аргумента. Введена А. Чёрчем (Church. 1941).