Это тривиализует исчисление

Это значит, что терминология функций должна остаться терминологией лямбда-исчисления, и ничего больше

Конечно, syntax driven, о каких ещё правилах вывода может идти речь

В смысле? CSP (давайте упростим)  описывает не функции, а поведения процессов.

вы имеете в виду, что можно доказать всё что угодно?

Ну вот || не syntax-driven, например. Можно выбрать произвольно из нескольких вариантов вывода.

Да. Возьмём соответствие Карри-Говарда. Это значит, что можно вычислить что угодно. В том числе противоречащие друг другу вещи.

А в чём проблема? Нам часто приходится вычислять такие вещи.

Ну, в обыденной жизни.

Я же писал: мы рассматриваем здесь пи-исчисление просто как некоторую теорию, оперирующую набором абстрактных символов, не привлекаем человеческих интерпретаций.

А теперь представь, что можно вычислить все противоречия (поправка в том, что парадокс Карри не пользуется негацией).

Не. Когда мы говорим о ЯП, как о языке программирования физических машин, мы не можем обойтись только лишь множеством формул.

Так то, что это противоречия, определяется лишь нашей интерпретацией. В природе вон полно противоречий. Взять противоречие между ОТО и КМ, например. И ничего, вычисляем и то, и другое, когда надо моделировать звёзды.

ну я по прежнему не понимаю, как это лишает нас возможности программировать на языке. Исходный тезис был в том, что нетипизированное лямбда-исчисление не годится для программирования т.к. выразим парадокс Карри.  На хаскеле вон тоже нельзя теоремы доказывать. И на С.

вычислить противоречие на практике это значит свалиться с ошибкой или уйти в бесконечный цикл

если мы доказываем корректность программы, то для нас это критическая проблема, но если мы пишем на условном эрланге, то это просто часть жизни

у жирара кстати в людике и позднейших системах есть специальные секвенты для обозначения "провалившихся доказательств" - daimon'ы

...а вы могли бы такого не писать?

Это про тип bottom? В нетипизированном лямбда-исчислении нет типов ) но противоречивые утверждения описать можно. Можно даже и не говорить о них — суть в том, что парадокс Карри позволяет вывести вообще что угодно. Например, грубо говоря, что это — строка и стул одновременно; с точки зрения логики противоречия тут нет, пока не заданы нужные определения, но нам не нужно этого делать, чтобы понять, что нам страшны не просто "это строка и не строка".

Это возникает из-за саморефлексивности нетипизированного лямбда-исчисления, которое не ограничено так, чтобы парадокс не возникал. Просто типизированное лямбда-исчисление создали как раз для того, чтобы уйти от парадоксов. И вот уже там можно найти тип bottom ) который значит больше, чем просто противоречие в логике, так как это прямо связывается с теорией вычислений.