judgement notation

• To: libor@ADELARD.MUNI.DCS.dcs.gla.ac.uk, types@dcs.gla.ac.uk
• Subject: judgement notation
• From: carl@research.att.com (Carl Gunter)
• Date: Mon, 9 Nov 92 14:06 EST
• Approved: types@dcs.gla.ac.uk

Libor Skarvads writes in response to a note from Andy Pitts:

>I prefer
>  \Gamma \rhd M : \tau      % \rhd is a small triangle pointing to the right
>to
>  \Gamma \vdash M : \tau    % \vdash is \TeX's name for  |-
>because `|-' is traditionally used for derivability of judgements, so
>  \vdash \Gamma \rhd M : \tau
>means that judgement $\Gamma \rhd M:\tau$ is derivable according to
>given rules.

It seems that there is an endless discussion to be had over the new
symbols that are being used to distinguish derivability (a relation)
from sequents (formal tuples) but let me venture a comment.  I see no
harm in using

 \Gamma |- M : tau,			(*)

as Andy proposed, to describe a ternary relation (the typing
judgement) between \Gamma, M and tau.  If one wants to focus on the
formal triple independently of whether it is derivable, then one can
substitute a triangle |> for the turnstile |-.  In most circumstances
this reduces the need for the cumbersome notation

  \vdash \Gamma \rhd M : \tau

which can be viewed as a longhand version of (*).

					--- carl gunter

• Prev: Notation query
• Next: Announcing "Lolli", An Interpreter for Linear-Logic Programming
• Index(es):
  • Main
  • Thread