We talked about this last night, but for the record/benefit of the audience:
Interestingly, higher-order judgment already has another meaning used by Twelf'ers, namely the judgment-level analogue of higher-order syntax:
lam : (exp -> exp) -> exp. % higher-order syntax
=>I : (true A -> true B) -> true (A => B). % higher-order judgment/syntax?
of/lam : ({x} of x A -> of (M x) B)
-> of (lam [x] M x) (A => B). % higher-order judgment
You said you'd just call this a "hypothetical judgment", which also makes sense (and is a kind of higher-order judgment itself!). Maybe we should call HOAS "hypothetical syntax"? :)
I think Frank uses "higher-level judgment" to describe your notion of "higher-order judgment": syntax is level 0, judgments about it are level 1, metatheorems are judgments at level 2, etc. A skew representation is one that mixes levels in the types of arguments, e.g. when your syntax requires proofs about syntax, or when your judgments themselves appeal to metatheorems.
no subject
Interestingly, higher-order judgment already has another meaning used by Twelf'ers, namely the judgment-level analogue of higher-order syntax:
lam : (exp -> exp) -> exp. % higher-order syntax =>I : (true A -> true B) -> true (A => B). % higher-order judgment/syntax? of/lam : ({x} of x A -> of (M x) B) -> of (lam [x] M x) (A => B). % higher-order judgmentYou said you'd just call this a "hypothetical judgment", which also makes sense (and is a kind of higher-order judgment itself!). Maybe we should call HOAS "hypothetical syntax"? :)
I think Frank uses "higher-level judgment" to describe your notion of "higher-order judgment": syntax is level 0, judgments about it are level 1, metatheorems are judgments at level 2, etc. A skew representation is one that mixes levels in the types of arguments, e.g. when your syntax requires proofs about syntax, or when your judgments themselves appeal to metatheorems.