Обычно ли обертывать переменную в бесполезный вызов `id`, чтобы избежать проблем с преобразованием eta на доказательствах?

Question

Используя язык, похожий на Morte/CoC, я пытаюсь доказать простое заявление there are lists of arbitrary lengths. Для этого я написал следующий вид:

∀ n:Nat -> 
(ThereIs (List Nat) 
    (Equal Nat 
    (List.length Nat l) 
    n))) 

ThereIs является зависимой пара (Sigma). Все закодировано в церкви. Чтобы доказать это, я написал следующее доказательство:

λ n:Nat -> 
(ThereIs.this (List Nat) 
    (λ l:(List Nat) -> (Equal Nat (List.length Nat l) n)) 
    (List.replicate Nat n Nat.Zero) 
    (Equal.refl Nat n)) 

Жутко, я получаю ошибку несоответствия типов между d (т.е. свободным переменным типом Nat) и λ c:* -> λ b:(c -> c) -> λ a:c -> (d c b a). Но этот более поздний термин, когда eta-reduced, равен d! Так как я не имею ETA-редуктор готов, вместо этого я сделал эту следующую функцию «бесполезной идентифицировать»:

λ n: Nat -> 

λ Nat:* -> 
λ Succ: (Nat -> Nat) -> 
λ Zero: Nat -> 

(n Nat Succ Zero) 

Теперь, применяя этот бесполезный идентификатор для каждого вхождения n, я «не-эта» это , в результате чего доказательство проверяется. Я хотел бы получить представление о том, что здесь происходит. Является ли эта «бесполезная функция id» известной/используемой моделью при написании доказательств? Почему не может быть исчисление конструкций, способное набрать это доказательство без этой небольшой помощи? Есть ли какие-либо глубокие аргументы в пользу этого явления или это просто то, что происходит по какой-то особой причине?

Answer 1

Вам необходимо добавить eta в ваш алгоритм проверки конверсий. Это может быть сделано несколько способов, самые простые два

• типа направлена ​​как на странице 22 Ulf Norell's thesis и используются в Agda
• Нетипизированные, используемые в Coq AFAIK

Нетипизированного ет преобразования полный для функций, и это также проще и быстрее, чем типизированная версия (нет необходимости перекомпилировать или кэшировать типы в нейтральных приложениях) в нашем случае. Алгоритм выглядит следующим образом:

Сначала мы проверяем случай, когда оба значения являются лямбдами, как обычно. Однако после этого мы проверяем два дополнительных случая, когда только одна сторона лямбда. В этих случаях мы применяем тело лямбды к новой общей переменной (как обычно), а также применяем другой термин к одной и той же переменной и проверяем равенство полученных значений.

Вот и все! Это на самом деле очень просто и не имеет большой производительности. Обратите внимание, что нам не нужно реализовывать eta-сокращение или сильную нормализацию eta, так как эта проверка преобразования легко выполняется по нормальным значениям слабой головки на лету.