switch to HOAS?

[jonsterling]

One problem with the current, fully-syntactic approach is that it's not possible to do anything with the syntheses of subgoals in the synthesis of the main goal except put them somewhere. This rules out "admissible rules", but even worse, it makes it impossible to do something like substitute a variable in one of the sub-syntheses.

The proper solution to this problem is not yet clear to me, but I wanted to record it here. I'm loath to switch back to full HOAS for everything, since it will make the implementation a zillion times more complex.

[jonsterling]

I think that even HOAS won't save me here, since then it would not be possible to accurately print subgoals. The real issue comes from dealing with judgments that have "generic" evidence. Consider the rule for implication:

x : A !- B true   <> !- A true
-------------------------------------cut
<> !- B true

The synthesis for the first premise is "generic", and it is important that I be able to substitute the synthesis of the second premise for x in the first in order to get the synthesis of the conclusion. This much can be done in HOAS. But what if the statement of the second premise contained something like [M/x]α, where α represents the synthesis of the first premise? Then, HOAS couldn't work, since if I try to print premise 2 by instantiating it at a fresh variable, the substitution would disappear.

It seems necessary, then, that the calculus should have some notion of explicit substitution that only gets evaluated on terms, not metavariables. @freebroccolo You've thought a lot more about metavariables and explicit substitutions than I have; does any of this make more sense to you than it does to me? Some of it seems related to these binding algebras.

[jonsterling]

First of all, we can define telescopes wrt. a metavariable context Θ as follows, as in the Fiore / Mahmoud stuff. First, let every object judgment J have a meta-arity SynthArity(J), which is the arity of its syntheses. For instance, SynthArity(A true) == 0, but SynthArity(x : A >> A true) == 1.

------------------------
Θ !- <> telescope

Θ, α : SynthArity(J) !- Ψ telescope
Θ :> . !- J term
--------------------------------------------------
Θ !- α:J, Ψ telescope

For any Ψ such that Ψ telescope, we can calculate a metacontext Metas(Ψ).

Metas(<>) := .
Metas(α:J, Ψ) := α:SynthArity(J), Metas(Ψ).

Then, the judgment J !!- τ => E -! Ψ would presuppose !- Ψ telescope and Metas(Ψ) :> . !- E term. With this in hand, we'll have side-stepped the issue of substitutions (I think).

[jonsterling]

Closing this because I have done two things:

1. switched to metavariables & valences (resolves inability to substitute in a goal)
2. switched to an "environment"-based approach (analogous to classic LCF validations), which allows the definition of admissible rules