Так вот я и спрашиваю: как именно это сделать для ||?

Берём аксиомы параллельной композиции и переписываем их в правила вывода 🤷‍♂

Так вот я и прошу показать, что получится?

Насчёт семантической примитивности / непримитивности.

В семантике логики первого порядка membership-отношение ZFC не описывается, а содержание этого отношения просто объявляется заключающимся только в аксиоматике ZFC, где фигурирует это отношение. Собственно, тут определять содержание предикатов теории множеств и не нужно.

Теория моделей для ZFC существует, но она сама опирается на теорию множеств. То есть, отношение всё ещё остаётся семантически не выраженным в других терминах, т.е. условия выполнимости членства не описывается в сторонних терминах как минимум потому, что сторонних терминов вообще нет. ZFC успешна в том числе по той причине, что позволяет говорить о моделях теорий множеств.

Зато мы можем выразить это отношение в терминах теории отображений (карт), которую можно выразить саму в терминах категориальной логики, и тогда мы получим формулировку условий выполнимости членства в категориальных терминах, и тогда это отношение в моей терминологии семантически непримитивно (хотя реальное содержание там на самом деле вообще никак не изменится).

Соответствующие данным аксиомам правила вывода

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

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

Это было бы круто.

Осталось IO написать на чистом Haskell.

Зачем?

Мы обсуждаем такую тему: достаточно ли одного только лямбда-исчисления для того, чтобы построить практичный ЯП.

Всякое добро туда можно натолкать встроенными функциями. Особенно, если стратегия исполнения ленивая.

Как и любые аксиомы, когда их превращают в правила вывода 🤷‍♂

Shift/reset ещё засунуть сразу

Если вы не хотите выходить за пределы языка, то ведь и С становится недостаточно.

Только ассемблер.

Хм... Я запутался, к сожалению. Верно ли я понимаю, что нам, всё же, понадобятся дополнительные правила вывода, которые не сведутся к правилам лямбда-исчисления?

От архитектуры микропроцессора зависит. На ARM достаточно, например.

По вашим требованиям это должно быть исчисление, которое может выразить пи-исчисление. Последнее Тьюринг-полно. Нетипизированное лямбда-исчисление Тьюринг-полно, но не годится как язык программирования из-за наличия парадоксального Y-комбинатора.

Точка входа - это не main.

Эмс. В Haskell вот или в ML этот комбинатор вшит в семантику.