[Prev][Next][Index][Thread]
Re: judgement notation
I think that the final reason I decided to use |> (\triangleright}
instead of |- in typing assertions/judgements such as
\Gamma |> M : \tau
is that it seems natural to right equations in the same form as
these assertions, as in
\Gamma |> M = N : \tau
Then we have the notational problem of saying one equation is
provable from another. For example, if E is a set of equations,
we might write
E |- \Gamma |> M = N : \tau
which, cumbersome as it may seem, is certainly better than
E |- \Gamma |- M = N : \tau.
In other words, it seems useful to write |> for a syntactic judgement,
and save |- for provabiility. (You might ask, why write the type assignment
\Gamma as part of the equation? The reason is, at least for the system
that is sound and complete for ccc's, the provability of \Gamma |> M=N
depends on \Gamma.)
Although a slight digression, I might comment that in Martin-Lof's systems
(at least historically), the distinction between well-formed and provable
judgements does not arise. There was never, to my knowledge,
a notion of ``well-formed but not provable judgement.'' However,
in a logical treatment of typed lambda calculus (of any kind),
I beleive there is a place for this distinction.
John Mitchell