Примером какого типа лямбда-исчисления может быть Лисп?

Lisp — это язык с динамической типизацией, будет ли это примерно соответствовать нетипизированному лямбда-исчислению?

Да, но только примерно. В «чистом» нетипизированном лямбда-исчислении все закодировано как функции. (Вы можете поискать в Google популярную «кодировку Черча» и менее популярную «кодировку Скотта».) В Лиспе есть нефункциональные данные, такие как атомы, числа и тому подобное, поэтому это будет считаться «нетипизированным лямбда-исчислением, расширенным константами».

Еще одно важное отличие заключается в порядке оценки. Правила сокращения членов лямбда-исчисления весьма недетерминированы. (Есть теорема, теорема Черча-Россера, которая в общих чертах говорит, что, пока что-то завершается, порядок вычисления не имеет значения.) На практике лямбда-члены обычно сокращаются с использованием крайнего слева-крайнего, также известного как редукция «нормального порядка», потому что если любая стратегия сокращения прекращает свое действие. Это очень отличается от Лиспа, который всегда оценивает аргументы в нормальной форме перед выполнением бета-редукции. Этот порядок оценки называется «коллировать по стоимости».

Таким образом, Лисп соответствует нетипизированному лямбда-исчислению с вызовом по значению, расширенному константами.

Джон Маккарти представил LISP в своей апрельской статье 1960 г. "Рекурсивные функции символьных выражений и их вычисление с помощью Машина, Часть I". Следующий абзац взят со страницы 6:

е. Функции и формы. В математике — за пределами математической логики — принято неточно использовать слово «функция» и применять его к таким формам, как y² + x. Поскольку позже мы будем производить вычисления с выражениями для функций, нам понадобится различие между функциями и формами и обозначение для выражения этого различия. Это различие и обозначение для его описания, от которого мы тривиально отклоняемся, дано Черчем [3].
...
3. ЧЕРЧ А. Исчисления лямбда-преобразования (Princeton University Press, Princeton, NJ, 1941).

Статья Википедии о лямбда-исчислении имеет историю публикаций Черча. Статья 1941 года, на которую ссылается Маккарти, похоже, посвящена типизированному лямбда-исчислению, что противоречит введению статьи в Википедии.

Ключевое слово lambda в Лиспе можно понять как относящееся к лямбда-исчислению только по аналогии. Лямбда-выражение Lisp — это тип анонимной функции.

Lisp — это не «лямбда-исчисление», я не знаю, что такое «лямбда-исчисление».

Если вы хотите идентифицировать лямбда-исчисления по системе типов, тогда Lisp, конечно, будет собственной системой. Ключевое слово «лямбда» в любом lisp до Scheme, безусловно, претенциозно, и после Scheme тоже есть место, чтобы сказать, что это так. Просто использовать «func» было бы более скромно. Lisp - это в основном процессор списков, а не «лямбда-исчисление».

Я также написал об этом довольно обширную статью, в которой пытался продемонстрировать, почему A: термин «функциональное программирование» бессмыслен и B: почему так же говорить о «лямбда-исчислении», а не о «системе типов»:

http://blog.nihilarchitect.net/archives/289/on-functional-programming/

Кроме того, имейте в виду, что в Лиспе все функции имеют один аргумент и могут иметь только списки в качестве аргументов.