У Клопа, ван Оострома и де Врийера есть статья о лямбда-исчислении с узорами.
http://www.sciencedirect.com/science/article/pii/S0304397508000571
В некотором смысле шаблон - это дерево переменных - хотя я просто думаю о нем как о вложенном кортеже переменных, например, ((x, y), z), (t, s)).
В статье они показали, что если шаблоны являются линейными в том смысле, что ни одна переменная в шаблоне не повторяется, то правило
(\p . m) n = m [n/p]
где p - переменная структура, а n - набор терминов с точно такой же формой, что и p, является слитым.
Мне любопытно, есть ли в литературе подобные разработки для лямбда-исчисления с шаблонами и дополнительным правилом eta (расширение, уменьшение или просто равенство).
В частности, под eta я имею в виду
m = \lambda p . m p
Точнее, мне любопытно, какими свойствами будет обладать такое лямбда-исчисление. Например, это ли слив?
Это заставляет классифицирующую категорию быть закрытой, потому что это заставляет свойство, которое
m p = n p implies m = n
Используя \ xi-правило между ними. Но, возможно, что-то могло пойти не так?
источник
Ответы:
Это не полный ответ; это комментарий, который стал слишком большим.
Если вы расширили типизированное лямбда-исчисление продуктами с проективными элиминаторами (то есть элиминаторами продуктов
fst(e)
и т. Д.snd(e)
), В принципе никаких проблем не возникнет. Причина, по которой это потребовалось так много времени, состоит в том, что оказывается, что более естественно делать этапы расширения, а не сокращения . См. Барри Джея « Добродетели расширения Эта» .Если вы хотите, чтобы в продуктах использовался шаблонный шаблон
Тогда дело обстоит сложнее. Основная сложность сопоставления с образцом - это коммутирующие преобразования . То есть эти исчисления имеют уравнение
и выяснить (а) какой контекст
C[-]
использовать и (б) как ориентировать это уравнение становится сложно. ИМО, современное состояние подходов в стиле переписывания - это перезапись экстремума Сэма Линдли с суммами и решающая эквивалентность Габриэля Шерера с суммами и пустой тип , оба из которых рассматривают типизированное лямбда-исчисление как с продуктами, так и с суммами.источник