Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Context schema subsumption #241

Open
MartyO256 opened this issue May 14, 2021 · 0 comments
Open

Context schema subsumption #241

MartyO256 opened this issue May 14, 2021 · 0 comments
Labels
A | core affecting the typechecker B | enhancement new features

Comments

@MartyO256
Copy link
Member

MartyO256 commented May 14, 2021

Context variable checking against context schemas should support schema subsumption.

Let schema G1 = some [...S1] block (...B1) and schema G2 = some [...S2] block (...B2) be context schemas, with lists S1, B1, S2, B2 of terms.
If every element of S2 is in S1, and every element of B2 is in B1, then G1 should be subsumed by G2.

Load the following Harpoon signature:

LF con : type =;
LF kind : type =;

LF cn-of : con -> kind -> type =;
LF kd-wf : kind -> type =;

LF kd-equiv : kind -> kind -> type =;

LF eterm : type =;
LF etp : type =;

LF unmap : eterm -> con -> type =;
LF tunmap : etp -> kind -> type =;
LF eof : eterm -> etp -> type =;
LF tequiv : etp -> etp -> type =;

schema conbind-reg =
  some [K : kind, wf : kd-wf K]
  block (a : con, da : cn-of a K);

schema unmap-bind =
  some [K : kind, Dwf : kd-wf K, B : etp, Dmap : tunmap B K]
  block (a : con, da : cn-of a K, x : eterm, dx : eof x B, xt : unmap x a);

proof kd-equiv-reg/1 :
  (g : conbind-reg)
  [g |- kd-equiv K1 K2] ->
    [g |- kd-wf K1] =
/ total 1 /
?
;

proof kd-equiv-reg/1' :
  (g : unmap-bind)
  [g |- kd-equiv K1 K2] ->
    [g |- kd-wf K1] =
/ total /
?
;

Theorems kd-equiv-reg/1 and kd-equiv-reg/1' are the same except for the context schema.

Schema unmap-bind should be subsumed by conbind-reg.
That is because some [K : kind, Dwf : kd-wf K, B : etp, Dmap : tunmap B K] contains at least the required terms some [K : kind, wf : kd-wf K] for instantiating the block in conbind-reg, and block (a : con, da : cn-of a K, x : eterm, dx : eof x B, xt : unmap x a) contains at least the terms in block (a : con, da : cn-of a K).

So, every block instantiation of unmap-bind can be used to instantiate conbind-reg whenever it is used in kd-equiv-reg/1.
Ideally, this context schema subsumption should also work irrespective of the topological ordering of terms in both some and block of either schemas.

kd-equiv-reg/1' should be trivially provable using kd-equiv-reg/1.
However, running the following Harpoon commands:

select kd-equiv-reg/1'
solve kd-equiv-reg/1 x

yields

Context variable
  _
doesn't check against schema
  unmap-bind = some [K : kind, wf : kd-wf K] block (a : con, da : cn-of a K)
@MartyO256 MartyO256 added B | enhancement new features A | core affecting the typechecker labels Jun 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A | core affecting the typechecker B | enhancement new features
Projects
None yet
Development

No branches or pull requests

1 participant