27
$\begingroup$

I am sorry if this is quite elementary question. But I always think, that why we use $:=$ at some places, instead of $=$. Is there any fundamental difference between these two? Before reading Terry Tao's blog (4 months ago), I had never seen a symbol like this (:=).

$\endgroup$
  • 7
    $\begingroup$ The former is usually used for definitions. This is adapted from some programming languages. The notation is deliberately unsymmetrical... $\endgroup$ – J. M. is not a mathematician Sep 11 '11 at 14:41
  • $\begingroup$ @J. M. Oh.. I too thought the same, but wasn't sure. Because my first year math books have definition notation of this type: $\displaystyle {{=}^{\mathrm{def}}}$. $\endgroup$ – gaurav Sep 11 '11 at 14:49
  • 3
    $\begingroup$ en.wikipedia.org/wiki/List_of_logic_symbols $\endgroup$ – Jack Sep 11 '11 at 15:03
  • 3
    $\begingroup$ I've also seen $\stackrel{\Delta}{=}$ used for definitions. I don't think there is an established notation in general; most just use $=$ and indicate that it is a definition rather than a relation in the surrounding text. $\endgroup$ – Rahul Sep 11 '11 at 15:32
24
$\begingroup$

Some authors like to distinguish the assertion "A is equal to B" from "define A as an object equal to B".

In math, the first one is always $A=B$ (I've never seen anything else, at least). But for definitions, I've seen

  1. $A \triangleq B$
  2. $A \equiv B$
  3. $A \stackrel{\mathrm{def}}{=} B$
  4. $A := B$

Often the triple equal sign is used for strong notions of equivalence (such as in binary relations) or with the "mod" symbol.

In computer programming, we are typographically limited of course. The assignment operator is usually distinguished from the comparison operator, and this is done in different ways depending on the language. For example in Pascal you assign x := 5 and compare x = 5. However in C you assign x = 5 and compare x == 5. (It should be noted that in C this syntax has caused untold confusion and a few famous bugs.)

My favorite (meaning "most awful") example is in PHP and javascript where one can do a "strict compare" with x === 5. Finally, some languages have ridiculous vagaries like distinguishing which comparision operator is used based on the type of variable (usually strings being different from numerics), with syntaxes like .eq. and related.

$\endgroup$
  • $\begingroup$ better answer! Thanks. $\endgroup$ – gaurav Sep 11 '11 at 15:37
  • $\begingroup$ "syntaxes like .eq. and related." - Heh... man, that sure was old... ;) $\endgroup$ – J. M. is not a mathematician Sep 11 '11 at 15:41
  • $\begingroup$ @J.M. Yeah, .eq. is FORTRAN77 (I'm showing my age here). $\endgroup$ – Fixee Sep 11 '11 at 15:42
  • $\begingroup$ I know; I've had the pleasure of re-implementing old code... :D $\endgroup$ – J. M. is not a mathematician Sep 11 '11 at 15:43
8
$\begingroup$

The notation := was used in some early programming languages. The meaning of x := 3 was "assign 3 to the variable x". So, the assignment could be distinguished from the the test if (x = 3) .... In mathematics the obvious meaning is "Let x be 3".

Modern programming languages use x = 3 for the assignment, and == for the equality test if (x == 3) ....

$\endgroup$
  • 4
    $\begingroup$ "Early" and "modern", eh? You may find some disagreement with those characterizations. $\endgroup$ – GEdgar Sep 11 '11 at 16:59
  • $\begingroup$ @Edgar: I know ... I did't find a better characterization at the moment of writing. I thought of Algol, Pascal with ':=', and Java, Javascript, C++, Python with '='. But I know the old C, Fortran with "=", etc. I wanted to say that I don't see ':=' so often today but surely there are some. Well, perhaps I should have written in some ones is ':=' and in other ones is '='. $\endgroup$ – Jiri Kriz Sep 11 '11 at 19:03
  • 2
    $\begingroup$ Mathematica uses := and = as (delayed and immediate) assignment operators, and == for equality comparisons. $\endgroup$ – J. M. is not a mathematician Sep 11 '11 at 21:37
  • $\begingroup$ Early and modern seems pretty accurate. Languages that don't use "==" for comparison or "=" for assignment could be called post-modern. :) $\endgroup$ – Andres Riofrio Mar 20 '12 at 18:48
  • 1
    $\begingroup$ Actually, = and := for assignment both date back to the dawn of high-level languages: FORTRAN used = in 1957, and ALGOL 58 used :=. Today the main distinction is between C-like syntax (with = and ==) and Pascal-like syntax (with := and =); C and Pascal were both initially developed in the early 1970s. It doesn't seem really meaningful do call that a distinction between "early" and "modern". $\endgroup$ – Henning Makholm Nov 11 '15 at 17:52
2
$\begingroup$

The equality symbol = denotes an operator that is part of the object theory. The definition symbol $\triangleq$ (and its variants) denotes a syntactic replacement, and is part of the metatheory.

This distinction is emphasized in the formal syntax of TLA+, whose axioms are those of Zermelo-Fraenkel set theory + Hilbert's $\varepsilon$, and functions. The theory has some axiom schemata for equality, as is usually the case with theories that include equality. In order to refer to symbols, they first have to be declared. For example:

CONSTANT a
VARIABLE x

THEOREM (a \in 1..2 /\ x = a) => (x \in 1..2)

Symbol a is declared to be a constant, and x as a variable (constants stay unchanged though a behavior, variables can change). The above theorem holds due to the indiscernibility of identicals (i.e., equal things "look the same").

A symbol can be defined, instead of declared. For example:

CONSTANTS a, b

Foo == a \/ b

The symbol Foo literally stands for a \/ b. The definition symbol == (typeset as $\triangleq$) is not an operator of the object theory, as \in, =, +, and other symbols are. It is metatheoretic notation that says that the string Foo abbreviates the expression a \/ b. So wherever Foo appears later, it is syntactically replaced by the expression a \/ b before any reasoning takes place.

Interestingly, there is another way of writing the last example:

CONSTANTS a, b

CONSTANT Foo
AXIOM Foo = (a \/ b)

What we have done is declare the identifier Foo as a constant, so some value in the object theory (here some set), and added an axiom that it so happens that the value of Foo is the same as the value of a \/ b (\/ denotes disjunction).

A defined symbol can be formally understood as shorthand for an extension by definition. The last example resembles an extension by definition that would correspond to the middle example. A clear introduction to the concept of extending a theory with definitions is given in Kunen's "Foundations of mathematics", Sec. II.15 on pages 148--152.

The theorem prover TLAPS has several examples of how definitions and declarations are used in its library of modules.

As a side note, $a \equiv b$ in TLA+ means $(a \in \mathrm{BOOLEAN}) \wedge (b \in \mathrm{BOOLEAN}) \wedge (a = b)$, and := means assignment in the algorithm language PlusCal, which translates to TLA+.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.