Я думаю, что я не понимаю этого, но ηη\eta -конверсия выглядит для меня как ββ\beta конверсия, которая ничего не делает, особый случай ββ\beta конверсии, где результатом является просто термин в лямбда-абстракции, потому что нечего делать, вид бессмысленного ββ\beta преобразования. Так что,...
Есть две основные, изученные теории лямбда-исчисления, теория бета и его Постполное расширение, теория бета-эта. Есть ли в этих двух теориях промежуточное, некое промежуточное правило, которое дает теорию переписывания слияния? Есть ли какое-то интересное понятие частичной экстенсиональности,...
Лемма: Предполагая, что эта эквивалентность у нас есть (\x -> ⊥) = ⊥ :: A -> B. Доказательство: ⊥ = (\x -> ⊥ x)по eta-эквивалентности и (\x -> ⊥ x) = (\x -> ⊥)по сокращению под лямбду. В отчете Haskell 2010, раздел 6.2, seqфункция определяется двумя уравнениями: seq :: a -> b...
У Клопа, ван Оострома и де Врийера есть статья о лямбда-исчислении с узорами. http://www.sciencedirect.com/science/article/pii/S0304397508000571 В некотором смысле шаблон - это дерево переменных - хотя я просто думаю о нем как о вложенном кортеже переменных, например, ((x, y), z), (t, s)). В статье...
Я перевожу книгу на LISP и, естественно, она затрагивает некоторые элементы калькуляции. Таким образом, понятие экстенсиональности упоминается там наряду с некоторыми моделями λ- вычисления, а именно: P ω и D ∞ (да, с бесконечностью вверху). И говорят, что P ω экстенсиональна, а D ∞...
Если у вас есть две функции, реализующие другой алгоритм сортировки, то можно ли по исходному коду сделать вывод, что они имеют одинаковые внешние свойства? Это означает, что у них обоих будет возможная несортированная последовательность в качестве входных данных и отсортированная...