Like the function, the value is a mechanism that assists in managing a set of axioms and laws. Value is used in simplifying the test for equality. Equality may be described as equality of value.
A value is the result of an evaluation function, which associates a value with an expression. It is a mapping from the domain of expressions to the domain of values.
For example,
![{\displaystyle \operatorname {value} [8*9]=72}](https://wikimedia.org/api/rest_v1/media/math/render/svg/54dbc93cfe773ac7c7508b3bf2f43c1aa625d36a)
![{\displaystyle \operatorname {value} [6*12]=72}](https://wikimedia.org/api/rest_v1/media/math/render/svg/beba418970878e1517dae22e65009d141d72d14c)
Therefore,
![{\displaystyle \operatorname {value} [8*9]=\operatorname {value} [6*12]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2438909803a97292df720ab6e0ffd968b6c79b29)
Values and evaluation provide a guiding principle for the application axioms to identify when expressions are equal.
Literal expressions edit
Where as an evaluation function interprets an expression as representing a value, a literal function interprets an expression as a formula or recipe for calculating a value, which has intrinsic identity. A literal expression is the result of the literal function, which associates a literal expression with an expression.
Value equality Literal equality
![{\displaystyle X=Y\iff \operatorname {value} [X]=\operatorname {value} [Y]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3e40053efbbdc0f39f30845f94ba63d013bb2fd7)
![{\displaystyle X\equiv Y\iff \operatorname {lit} [X]=\operatorname {lit} [Y]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aff588ab713d2bc4419dbf0178fee42b89b28f6c)
When we say that two expressions are equal we mean there values are equal.
When we say that two expressions are identical we mean there literal expressions are equal. For example the following two expressions are regarded as identical, because the name of subscript does not effect the meaning of the function.
There are three domains described here;
Domain of expressions Domain of values Domain of literal expressions
![{\displaystyle \operatorname {lit} [3*7]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3ca00d719e294cb8c5dd7fe75636fbb92dd9f48f)
![{\displaystyle \operatorname {lit} [83]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ec810f7b9b3b7255682542436c1f11de4926cf2e)
In each domain, equality may be defined differently.
Values as literal expressions edit
One possibility is for values to be equated with a subset of the literal expressions. These expressions are identified by a function
![{\displaystyle C[X]\land C[Y]\to (X=Y\iff lit[X]=lit[Y])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5593dcaca35c041ed77d5e15f108d08c2491f63a)
or
![{\displaystyle C[X]\land C[Y]\to (X=Y\iff X\equiv Y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c34c5752a80f33ee04f791639a695eff2caee26a)
The function C identifies which expressions represent values. This is the approach used in arithmetic.
An example from arithmetic edit
Familiarity with arithmetic makes it hard to recognise the role of a value in making a calculation. To bring attention to the issue the following trivial example is taken apart in detail.
Suppose C is defined so that on a number it returns true and for other functions false. Then,
![{\displaystyle C[60]=\top }](https://wikimedia.org/api/rest_v1/media/math/render/svg/ab795a9c0ed6c05c4165d5b8cf00ccccf353114b)
![{\displaystyle C[5*12]=\bot }](https://wikimedia.org/api/rest_v1/media/math/render/svg/bd0b282b5fe9175aead546457239a42721eb0c62)
![{\displaystyle C[3*20]=\bot }](https://wikimedia.org/api/rest_v1/media/math/render/svg/89daaf59757fa32a39d4c431ba47ba9d359480a9)
For example to evaluate,
Then,
![{\displaystyle C[60]\land C[60]\to (60=60\iff 60\equiv 60)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ceb7a72113b3d090c79b6164de3af7bbc2a98d93)
And as 60 is identical to 60 the expressions are equal.
Literal expressions as values edit
To use literal expressions as values, a subset of literal expressions must be identified. All operators must be shown to have values already represented in the set (the set is closed under the operation). A single literal expression must be identified for each element in the set and the function C must be defined to identify those literal expressions.
From values to mappings edit
Once values have been defined the function may be defined as the mapping from a values to values. Functions also provide a guiding principle for evaluation.