Proposal for proof language #87
Conversation
| abstract def well_formed: | ||
| ... | ||
|
|
||
| abstract class Pattern(Term): |
There was a problem hiding this comment.
Maybe consider adding Contexts that should have the distinguished hole variable check, as we discussed?
There was a problem hiding this comment.
I'm not sure I recall what we discussed. MetaVars already have an application_context field that is used for this check.
| * Supporting: | ||
|
|
||
| `List n:uint32` | ||
| : Consume $n$ items from the stack, and push a list containing those items to the stack. |
There was a problem hiding this comment.
Add the explanation we discussed, please.
|
|
||
| * Variables and Symbols: | ||
|
|
||
| `EVar <uint32>` |
There was a problem hiding this comment.
Let's think about whether this should pop from the stack instead (adding this comment just for reference).
|
|
||
| # Meta-requirements that must be satisfied by any instantiation. | ||
| fresh: list[EVar | SVar] # variables that must not occur in an instatiation | ||
| positive: list[SVar] # variables that must only occur positively in an instatiation |
There was a problem hiding this comment.
Shouldn't at least positive, negative rather be in Pattern? Pattern also have positive/negative occurrences of variables, there's little reason why we should compute them. These could also be actual references in the concrete pattern.
There was a problem hiding this comment.
I'm not sure I follow. For concrete patterns, we don't need additional metadata to know whether something is positive or negative. We can just look at the term and check. For metavariables, that is not the case, since we cannot see "inside" the metavariable.
Note that a smart implementation, may keep track of positivity/negativity track in a clever way. That is not our concern here. This is not an implementation, its a specification of the language.
There was a problem hiding this comment.
Fair enough, it's a specification. I was pointing more to the current python implementation.
It is a bit redundant if you can hold direct references to them. Especially later on when we want to do substitutions more efficiently. But sure, we can do optimizations later.
| name: int | ||
| fresh: tuple[EVar | SVar, ...] | ||
| positive: tuple[SVar, ...] | ||
| negative: tuple[SVar, ...] |
There was a problem hiding this comment.
Why do we have both 'positive' and 'negative', when an occurrence of a variable can only be either positive or negative? Is this for performance reasons?
There was a problem hiding this comment.
We need both to be able to prove the other, since they are only defined mutually. Note that a variable meets both positivity and negativity if it does not occur at all.
There was a problem hiding this comment.
So if it's in both, it does not occur, if it is in one of them, it is positive/negative, and if it is in neither of them, then it is undefined?
No description provided.