Многие учебники охватывают типы пересечений в лямбда-исчислении. Правила набора для пересечения могут быть определены следующим образом (поверх простого типа лямбда-исчисления с подтипами):
Типы пересечений имеют интересные свойства в отношении нормализации:
- Лямбда-член можно вводить без использования если оно сильно нормализуется.
- Лямбда-член допускает тип, не содержащий если он имеет нормальную форму.
Что если вместо добавления пересечений мы добавим объединения?
Есть ли у лямбда-исчисления с простыми типами, подтипами и объединениями какое-нибудь интересное подобное свойство? Как можно охарактеризовать термины, которые можно набрать с помощью union?
lambda-calculus
type-theory
logic
Жиль "ТАК - перестань быть злым"
источник
источник
Ответы:
В первой системе то, что вы называете подтипом, это два правила:
Они соответствуют правилам исключения для ; без них or более или менее бесполезна.∧∧ ∧
Во второй системе (со связями и , к которой мы могли бы также добавить ), вышеприведенные правила подтипов не имеют значения, и я думаю, что вы имели в виду следующие сопутствующие правила:→ ⊥∨ → ⊥
Для чего это стоит, эта система позволяет набирать (используя правило rule ), которое нельзя набирать простыми типами, которое имеет нормальную форму, но не сильно нормализует ,⊥ E( λ х . I) Ω : A → A ⊥ E
Случайные мысли: (возможно это стоит спросить на TCS)
Это приводит меня к предположению, что связанные свойства являются чем-то вроде:
Упражнение: докажи, что я не прав.
Кроме того, это похоже на вырожденный случай, может быть, нам стоит подумать о добавлении этого парня в картину. Насколько я помню, это позволило бы получить ?A ∨ ( A → ⊥ )
источник
Я просто хочу объяснить, почему типы пересечений хорошо подходят для характеристики классов нормализации (сильных, головных или слабых), тогда как другие системы типов не могут. (простой тип или система F).
Вот почему я не думаю, что есть легкая характеристика нормализации для типов объединения.
источник