Простое типизированное лямбда-исчисление и логика высшего порядка

11

Какова связь между просто типизированным лямбда-исчислением и логикой более высокого порядка?

При Карри-Говарде кажется, что просто типизированное лямбда-исчисление соответствует логике высказываний. Как это связано с логикой высшего порядка? Согласно этому руководству Geuvers: http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf язык HOL выглядит как STT. Разве это не должно быть PROP? Что это значит?

Имел ли в виду Церковь HOL при определении STT?

lambda2
источник
6
Да, Церковь действительно имела в виду HOL. Хитрость в получении HOL от STT состоит в том, чтобы использовать равенство в дополнение к применению функции и абстракции функции. Тогда вы можете написать как ( λ x : α . A ) = ( λ x : α . ) , среди прочих. Мне нравится «Семь достоинств теории простого типа» как введение в STT, в котором рассматриваются вопросы такого рода. Может быть, я должен написать ответ ...(Икс:α,A*)(λИкс:α,A*)знак равно(λИкс:α,)
Томас Климпел
Итак, говоря о Карри-Ховарде, что будет правильным логическим эквивалентом STT? ХОЛ или ПРОП?
lambda2
Что касается Curry-Howard, то не думаю, что это будет HOL. Может быть, это мультипликативный фрагмент интуиционистского PROP, то есть интуиционистский PROP без «или». Но это было для ССС (декартовой закрытой категории), и я немного устал в данный момент. Лямбда, вероятно, будет переводиться как «импликация», которая была «экспоненциальной» в КХЦ. «Продукт» из CCC был «и», так что для этого вам понадобится «пара» в STT. И тогда «или» будет типом «сумма» в STT, т. Е. Дизъюнктное объединение, может быть, если «a», то «b», иначе «c» делает это.
Томас Климпел
Я думаю, что я что-то путаю (или все). Если STT ~ = PROP (через Curry-Howard) и STT также является HOL, тогда я могу использовать PROP в некотором смысле, чтобы иметь HOL?
lambda2
1
@ThomasKlimpel: вы должны превратить ваши комментарии в ответ.
Cody

Ответы:

10

Различие заключается в следующем: если STLC принимается как примитивный язык на конструкторах добавления на уровне типов и достаточно небольшого числа аксиом, чтобы дать вам полную выразительную силу HOL.

Взяв за базовый тип чисел ans ο за базовый тип предложений, вы можете добавить константы τ : ( τ ο ) οιο

τ:(το)ο⊃:οοο

где - произвольный тип (так что одна константа для каждого типа). Один возможный набор аксиом:τ

φ(Икс)τ(λИкс,φ(Икс))Икс:τ не свободен в гипотезах

[ψ],,,φψφ

[ψ]ψτ,

λ

λ

Коди
источник
1
τзнак равноτ:ττο
Что это за умные аксиомы, пожалуйста? Я предполагаю, что это связано с предоставлением способа доказать равенство ... Кроме того, знаете ли вы имя для явного различения уровней расширений HOL? (с равенством, затем с полиморфным типом, затем с зависимыми типами).
Hibou57
1
@ Hibou57 аксиомы описаны в превосходной статье «Семь достоинств теории простого типа» . Я не знаю, что существуют явные имена, чтобы отличать разные расширения STT, кроме тех, которые вы использовали.
Коди