Algorithmic Equality in the Polymorphic -Calculus
For these examples, I will use a simplified version of the ORBI benchmark. We do not need to reason about declarative equality to bring out the differences between Beluga and Adelfa’s handling of schema subsumption.
Adelfa Version
Signature
tp : type.
arr : {T1:tp}{T2:tp} tp.
all : {T:{ T':tp} tp} tp.
tm: type.
lam: {M: tm -> tm} tm.
tlam : {M: tp -> tm} tm.
app: {M1:tm}{M2:tm} tm.
tapp : {M:tm}{T:tp} tm.
atp : {T1:tp}{T2:tp} type.
aeq: {M1:tp}{M2:tp} type.
atp_arr : {T1:tp}{T2:tp}{S1:tp}{S2:tp}
{D1:atp T1 T2}
{D2:atp S1 S2}
atp (arr T1 S1) (arr T2 S2).
atp_all : {T1:{T1':tp} tp}{T2: {T2':tp} tp}
{D: {T:tp} atp T T -> atp (T1 T) (T2 T)}
atp (all ([x] T1 x)) (all ([x] T2 x)).
ae_a : {M1: tm}{M2: tm}{N1:tm}{N2:tm}
{D1:aeq M1 N1}{D2:aeq M2 N2}
aeq (app M1 M2) (app N1 N2).
ae_ta : {M1: tm}{M2: tm}{T1:tp}{T2:tp}
{D1:aeq M1 M2}{D2:atp T1 T2}
aeq (tapp M1 T1) (tapp M2 T2).
ae_l : {M: tm -> tm}{N: tm -> tm}
{D: {z:tm} aeq z z -> aeq (M z) (N z)}
aeq (lam ([x] M x)) (lam ([x] N x)).
ae_tl : {M: tp -> tm}{N: tp -> tm}
{D: {z:tp} atp z z -> aeq (M z) (N z)}
aeq (tlam ([x] M x)) (tlam ([x] N x)).
Development
Specification "poly-equal-min.lf".
Schema atpCtx := (t:tp, dt:atp t t).
Theorem reflTp : ctx G:atpCtx, forall T,
{G |- T : tp} => exists D, {G |- D : atp T T}
induction on 1 intros
case H1 weaken H2 with atp n n apply IH to H3 with (G = G, n1:tp, n:atp n1 n1)
exists atp_all T1 T1 D search
apply IH to H2 apply IH to H3
exists atp_arr T1 T1 T2 T2 D D1 search
exists n1 search
% This schema is fine to use in place of atpCtx for G in reflTp
Schema aeqCtx := (x:tm, dx:aeq x x);
(t:tp, dt:atp t t).
Theorem ref : ctx G:aeqCtx, forall M,
{G |- M : tm} => exists D, {G |- D : aeq M M}
induction on 1 intros
case H1
apply reflTp to H3 abort
% This schema is not fine to use in place of atpCtx for G in reflTp
% If we were to try and prove this in reflTp, the variable case would not be possible!
Schema aeqCtxErr:= (x:tm, dx:aeq x x);
(t:tp, dt:atp t t);
(t:tp).
Theorem ref : ctx G:aeqCtxErr, forall M,
{G |- M : tm} => exists D, {G |- D : aeq M M}
induction on 1 intros
case H1
% Notice Adelfa reports an error here and does not update the state
apply reflTp to H3
Beluga
I’ve modified Beluga’s version here. I’ve introduced the same aeqCtxErr
into the development. Instead of reporting any issues, it will accept the usage
of the reflTp
lemma in ref
. I’ve highlighted the line where the
incorrect call is made.
soundness.bel
LF tp : type =
| arr : tp -> tp -> tp
| all : (tp -> tp) -> tp
;
--name tp T a.
LF term: type =
| app : term -> term -> term
| lam : (term -> term) -> term
| tlam: (tp -> term) -> term
| tapp: term -> tp -> term
;
--name term M x.
LF atp: tp -> tp -> type =
| at_al : ({a:tp} atp a a -> atp (T a) (S a)) -> atp (all T) (all S)
| at_arr: atp T1 T2 -> atp S1 S2 -> atp (arr T1 S1) (arr T2 S2)
;
--name atp Q u.
LF aeq: term -> term -> type =
| ae_a : aeq M1 N1 -> aeq M2 N2 -> aeq (app M1 M2) (app N1 N2)
| ae_l : ({x:term} aeq x x -> aeq (M x) (N x)) -> aeq (lam (\x. M x)) (lam (\x. N x))
| ae_tl: ({a:tp} atp a a -> aeq (M a) (N a)) -> aeq (tlam (\a. M a)) (tlam (\a. N a))
| ae_ta : aeq M N -> atp T S -> aeq (tapp M T) (tapp N S)
;
--name aeq D u.
schema atpCtx = block a:tp , _t:atp a a;
schema aeqCtx = block (x:term, _u:aeq x x) + block (a:tp, _t:atp a a);
schema aeqCtxErr = block (x:term, _u:aeq x x) + block (a:tp, _t:atp a a) + block (a:tp);
rec reftp : {gamma:atpCtx} {T:[gamma |- tp]} [gamma |- atp T T] =
mlam gamma => mlam T => case [gamma |- T] of
| [gamma |- #p.1] => [gamma |- #p.2]
| [gamma |- all \x. T] =>
let [gamma, b:block a:tp , _t:atp a a |- D[.., b.1, b.2]] =
reftp [gamma, b:block a:tp , _t:atp a a] [gamma, b |- T[.., b.1]]
in
[gamma |- at_al \x. \w. D]
| [gamma |- arr T S] =>
let [gamma |- D1] = reftp [gamma] [gamma |- T] in
let [gamma |- D2] = reftp [gamma] [gamma |- S] in
[gamma |- at_arr D1 D2]
;
rec ref : {gamma:aeqCtx} {M:[gamma |- term]} [gamma |- aeq M M] =
mlam gamma => mlam M => case [gamma |- M] of
| [gamma |- #p.1] => [gamma |- #p.2]
| [gamma |- lam \x. M] =>
let [gamma, b:block y:term , _t:aeq y y |- D[.., b.1, b.2]] =
ref [gamma, b:block y:term , _t:aeq y y] [gamma, b |- M[.., b.1]]
in
[gamma |- ae_l \x. \w. D]
| [gamma |- app M1 M2] =>
let [gamma |- D1] = ref [gamma] [gamma |- M1] in
let [gamma |- D2] = ref [gamma] [gamma |- M2] in
[gamma |- ae_a D1 D2]
| [gamma |- tlam \a. M] =>
let [gamma, b:block a:tp , _t:atp a a |- D[.., b.1, b.2]] =
ref [gamma, b:block a:tp , _t:atp a a] [gamma, b |- M[.., b.1]]
in
[gamma |- ae_tl \x. \w. D]
| [gamma |- tapp M T] =>
let [gamma |- D1] = ref [gamma] [gamma |- M] in
let [gamma |- D2] = reftp [gamma] [gamma |- T] in
[gamma |- ae_ta D1 D2]
;
rec refErr : {gamma:aeqCtxErr} {M:[gamma |- term]} [gamma |- aeq M M] =
mlam gamma => mlam M => case [gamma |- M] of
| [gamma |- #p.1] => [gamma |- #p.2]
| [gamma |- lam \x. M] =>
let [gamma, b:block y:term , _t:aeq y y |- D[.., b.1, b.2]] =
ref [gamma, b:block y:term , _t:aeq y y] [gamma, b |- M[.., b.1]]
in
[gamma |- ae_l \x. \w. D]
| [gamma |- app M1 M2] =>
let [gamma |- D1] = ref [gamma] [gamma |- M1] in
let [gamma |- D2] = ref [gamma] [gamma |- M2] in
[gamma |- ae_a D1 D2]
| [gamma |- tlam \a. M] =>
let [gamma, b:block a:tp , _t:atp a a |- D[.., b.1, b.2]] =
ref [gamma, b:block a:tp , _t:atp a a] [gamma, b |- M[.., b.1]]
in
[gamma |- ae_tl \x. \w. D]
| [gamma |- tapp M T] =>
let [gamma |- D1] = ref [gamma] [gamma |- M] in
let [gamma |- D2] = reftp [gamma] [gamma |- T] in
[gamma |- ae_ta D1 D2]
;
Running Beluga on this erroneous development doesn’t report any errors.
$ beluga soundness.bel
## Type Reconstruction begin: soundness.bel ##
## Type Reconstruction done: soundness.bel ##