Я пытаюсь реализовать функцию extract, которая принимает выражение типа (f (g x y)) вместе с переменной, например y, и создает функцию y --> (f (g x y)) с комбинаторами SKI. В этом случае результат должен быть (S (K f) (g x)).
В каком-то смысле я делаю преобразование из лямбда-термина в его версию SKI.
I 'Я пытаюсь сделать типизированную версию этого, и у меня трудные времена.
Настройка
Типы в этих выражениях представлены следующим индуктивным типом
Inductive type : Type :=
| base_type : forall (n : nat), type
| arrow_type : type -> type -> type.
По сути, у меня есть несколько базовых типов, проиндексированных целыми числами (base_type), а также я могу создавать типы функций между ними (arrow_type)
Ввести нотацию для типов функций
Notation "A --> B" := (arrow_type A B) (at level 30, right associativity).
Выражения представлены следующим индуктивным типом
Inductive term : type -> Type :=
| var : forall (n : nat) (A : type), term A
| eval : forall {A B : type}, term (A-->B) -> term A -> term B
| I : forall (A : type) , term (A --> A)
| K : forall (A B : type) , term (A --> (B --> A))
| S : forall (A X Y : type), term ((A --> X --> Y) --> (A --> X) --> A --> Y).
Здесь я снова имею набор базовых переменных, индексированных целыми числами n : nat и типом A : type (не Type!)
Таким образом, переменная x : term X является выражением с type X.
Чтобы уменьшить болевые ощущения, давайте введем нотацию для оценки функции
Notation "f [ x ]" := (eval f x) (at level 25, left associativity).
Вводный пример
Исходный вопрос можно сформулировать более точно следующим образом.
Давайте начнем с определения с некоторых типов
Notation X := (base_type 0).
Notation Y := (base_type 1).
Определение переменных x y и функций f g (все они могут быть проиндексированы с 0, поскольку все они имеют разные type)
Notation x := (var 0 X).
Notation y := (var 0 Y).
Notation g := (var 0 (X --> Y --> X)).
Notation f := (var 0 (X --> Y)).
Полученное выражение type равно Y.
Check f[g[x][y]].
Моя цель - создать функцию extract такую, что
extract f[g[x][y]] y
производит
S[K[f]][g[x]]
с заполненным типом
(S Y X Y)[(K (X-->Y) Y)[f]][g[x]]
Равенство по type и term
Для продолжения определения extract Мне нужно определить равенство для type и term.
Require Import Arith.EqNat.
Open Scope bool_scope.
Fixpoint eq_type (A B : type) : bool :=
match A, B with
| base_type n, base_type m => beq_nat n m
| arrow_type X Y, arrow_type X' Y' => (eq_type X X') && (eq_type Y Y')
| _, _ => false
end.
Fixpoint eq_term {A B : type} (a : term A) (b : term B) : bool :=
match a, b with
| var n X , var n' X' => (beq_nat n n') && (eq_type X X')
| eval X Y f x , eval X' Y' f' x' => (eq_type X X') && (eq_type Y Y') && (eq_term f f') && (eq_term x x')
| I X , I X' => (eq_type X X')
| K X Y , K X' Y' => (eq_type X X') && (eq_type Y Y')
| S Z X Y , S Z' X' Y' => (eq_type X X') && (eq_type Y Y') && (eq_type Z Z')
| _ , _ => false
end.
Попытка реализации extract
«Реализация» довольно проста
Fixpoint extract {A B : type} (expr : term B) (val : term A) : term (A-->B) :=
if (eq_term expr val)
then (I A)
else
match expr with
| eval X Y f x => (S A X Y)[extract f val][extract x val]
| _ => (K B A)[expr]
end.
Есть две проблемы
- При возврате
I A: type из I A равно A --> A не A --> B, как обещано, но в этом конкретном случае я должен бытьвозможность доказать, что B и A одинаковы. - При возврате
(S A X Y)[...: возвращаемое значение равно A --> Y, а не A --> B, но опять же я должен бытьспособен доказать, что Y равно B.
Как я могу доказать B=A и Y=B в тех конкретных случаях, когда определение функции принимается?