Разрешима ли проблема решения для свободной бидекартовой замкнутой категории (BCCC)? Эквивалентно, разрешимо ли равенство для простого лямбда-исчисления, расширенного сильными n-мерными произведениями и суммами? Проблема решения для свободного почти BCCC разрешима:
http://www.cs.nott.ac.uk/~txa/publ/lics01.pdf
Но эта работа не включает начальный объект или пустой тип в терминах лямбда-исчисления, хотя они предполагают, что их метод может распространяться на BCCC.
Я хотел указать вам на эту тему на Список рассылки TYPES для ответа, но я вижу, что вы были тем, кто его инициировал :).
Я дам частичный ответ, который поможет проиллюстрировать, почему исходный объект исключается. Все начинает рушиться, когда исходные объекты объединяются с экспонентами; или терминальные объекты с коэкспоненциалами. Этот коллапс становится полным, когда присутствуют как экспоненциальные, так и коэкспоненциальные; в этом случае проблема разрешимости становится тривиальной, сводящейся к доказуемости в логике, в то время как проблема приведения к нормальной форме становится более сложной - по иронии судьбы.
Я разместил более подробную информацию здесь. Я не могу ответить на него здесь, потому что ложноположительная ошибка неправильно отформатированного кода в StackOverflow делает его интерфейс не подлежащим ремонту. (Я понимаю это даже для пустого окна дисплея, и в моем ответе нет компьютерного программирования, поскольку это даже не компьютерный вопрос!)
https://math.stackexchange.com/questions/4032422/decidability-of-bi-cartesian-closed-categories
