[Prev][Next][Index][Thread]

Question about notation




In article <Bx6xoC.9vK@dcs.glasgow.ac.uk> wand@edu.northeastern.ccs.dec5120z (Mitchell Wand) writes:

	x1 has type tau-1, x2 has type tau-2,...,xn has type tau-n ?

      I have heard these sets sometimes called a BASIS, sometimes an
      ENVIRONMENT, sometimes a CONTEXT, etc. Any consensus?

   I tend to call one of these "a set of type assumptions", though the singular
   "type assumption" would be better.  [I usually use the meta-variable A to
   range over them].

I believe that in Type Theory the word context is now more or less
standard (many people also seem to use \Gamma as a meta-variable).
"Set" doesn't seem right because if you have dependent types you can't
reorder your context arbitrarily.
--

 Thorsten Altenkirch         	And there's a hand, my trusty fiere,
 Laboratory for Foundations  	   And gie's a hand o' thine,
 of Computer Science 	      	And we'll tak a right guid-willie waught
 University of Edinburgh     	   For auld lang syne!