[Search for users] [Overall Top Noters] [List of all Conferences] [Download this site]

Conference rusure::math

Title:	Mathematics at DEC

Moderator:	RUSURE::EDP

Created:	Mon Feb 03 1986
Last Modified:	Fri Jun 06 1997
Last Successful Update:	Fri Jun 06 1997
Number of topics:	2083
Total number of notes:	14613

887.0. "Expressing enumerated types" by DEC::LEONARD (VAX Architecture Management) Fri Jun 17 1988 19:28

    Mathematical logic has standard notations for some things--backward E
    for existential quantification, for example.  Is there a standard
    notation for an enumerated type?  I'm writing a paper in which I create
    a new type, "reference", which can have the values "read" and "write".
    If it were boolean, I'd just say: 
    
    	reference: bool
    
    (with "bool" in boldface) and I'd expect my audience to know what
    I was saying.  But how do I express the definition of an enumerated
    type?  If there isn't a well-known notation, I'll probably use
    
    	reference: { read | write }
    
    but if there is a standard notation, I should use it instead.

T.R	Title	User	Personal Name	Date	Lines
887.1		CLT::GILBERT		`Fri Jun 17 1988 20:33`	8
	Good question. How about: reference e { read, write } where the 'e' is the epsilon character, indicating "is a member of", { ... } is a set expression, and 'read' and 'write' are considered to be literals (you might have literals in boldface or some other font).
887.2		DEC::LEONARD	VAX Architecture Management	`Mon Jun 20 1988 13:52`	7
	Yup, I can do that. It'll actually be a tad confusing, since I'm using Hilbert's epsilon operator already. (Hilbert's epsilon is very much like ThereExists, but it returns not a truth value, but a value of the same type as the bound variable. I pronounce it "an example such that". If a value exists meeting the specified constraint, then one such value is returned, and if no value exists, then any value of the same type is returned.)
887.3		ULTRA::ELLIS	David Ellis	`Thu Jun 23 1988 20:14`	12
	To me, an enumerated type is a finite set. So I'd simply say reference = {read, write}. Something of type reference is an element of the set, of course. Your use of Hilbert's epsilon operator is very interesting. Many systems that don't have this operator leave the user twisting to express instances. There are lots of different names for this operator. Quine used an inverted iota, and I've also seen it known as the "witness" operator, denoted by the symbol gamma and used like another flavor of quantifier. Extremely useful. (I Wish it were in Ina Jo).