Editing Expression (mathematics) (section)

== Formal definition ==
The term 'expression' is part of the [[language of mathematics]], that is to say, it is not defined ''within'' mathematics, but taken as a [[Primitive notion|primitive]] part of the language. To attempt to define the term would not be doing mathematics, but rather, one would be engaging in a kind of [[metamathematics]] (the [[metalanguage]] of mathematics), usually [[mathematical logic]]. Within mathematical logic, mathematics is usually described as a kind of [[formal language]], and a well-formed expression can be [[Recursive definition|defined recursively]] as follows:<ref name="Model Theory"/>

The [[Alphabet (formal languages)|alphabet]] consists of:

* A set of individual [[Constant (mathematics)|constants]]: Symbols representing fixed [[Mathematical object|objects]] in the [[domain of discourse]], such as [[Numeral system|numerals]] (1, 2.5, 1/7, ...), [[Set (mathematics)|sets]] (<math>\varnothing, \{1,2,3\}</math>, ...), [[truth values]] (T or F), etc.
* A set of individual variables: A [[Countable set|countably infinite]] amount of symbols representing [[Variable (mathematics)|variables]] used for representing an unspecified object in the domain. (Usually letters like {{mvar|x}}, or {{mvar|y}})
* A set of operations: [[Function symbols]] representing [[Operation (mathematics)|operations]] that can be performed on elements over the domain, like addition (+), multiplication (×), or set operations like union (∪), or intersection (∩). (Functions can be understood as [[unary operations]])
* Brackets ( )

With this alphabet, the recursive rules for forming a well-formed expression (WFE) are as follows:

* Any constant or variable as defined are the [[atomic formula|atomic expressions]], the simplest well-formed expressions (WFE's). For instance, the constant <math>2</math> or the variable <math>x</math> are syntactically correct expressions.
* Let <math>F</math> be a [[metavariable]] for any [[n-ary operation]] over the domain, and let <math>\phi_1, \phi_2, ... \phi_n</math> be metavariables for any WFE's.
:Then <math>F(\phi_1, \phi_2, ... \phi_n)</math> is also well-formed. For the most often used operations, more convenient notations (like [[infix notation]]) have been developed over the centuries.
:For instance, if the domain of discourse is the [[real number]]s, <math>F</math> can denote the [[binary operation]] +, then <math>\phi_1 + \phi_2</math> is well-formed. Or <math>F</math> can be the unary operation <math>\surd</math> so <math>\sqrt{\phi_1}</math> is well-formed.
:Brackets are initially around each non-atomic expression, but they can be deleted in cases where there is a defined [[order of operations]], or where order doesn't matter (i.e. where operations are [[Associative property|associative]]).

A well-formed expression can be thought as a [[Abstract syntax tree|syntax tree]].<ref>{{cite book |last1=Hermes |first1=Hans |author-link=Hans Hermes |title=Introduction to Mathematical Logic |publisher=Springer London |year=1973 |isbn=3540058192 |issn=1431-4657}}; here: Sect.II.1.3</ref> The [[Node (computer science)|leaf nodes]] are always atomic expressions. Operations <math> + </math> and <math> \cup </math> have exactly two child nodes, while operations <math display="inline">\sqrt{x} </math>, <math display="inline">\text{ln}(x)</math> and <math display="inline"> \frac{d}{dx} </math> have exactly one. There are countably infinitely many WFE's, however, each WFE has a finite number of nodes.

===Lambda calculus===
{{Main|Lambda calculus}}

Formal languages allow [[Formal system|formalizing]] the concept of well-formed expressions.

In the 1930s, a new type of expression, the [[Lambda calculus#Definition|lambda expression]], was introduced by [[Alonzo Church]] and [[Stephen Kleene]] for formalizing [[function (mathematics)|function]]s and their evaluation.<ref>{{cite journal|first=Alonzo|last=Church|author-link=Alonzo Church|title=A set of postulates for the foundation of logic|journal=Annals of Mathematics|series=Series 2|volume=33|issue=2|pages=346–366|year=1932|doi=10.2307/1968337|jstor=1968337}}</ref>{{efn|For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).}} The lambda operators (lambda abstraction and function application) form the basis for lambda calculus, a formal system used in [[mathematical logic]] and [[programming language theory]].

The equivalence of two lambda expressions is [[decision problem|undecidable]] (but see [[unification (computer science)]]). This is also the case for the expressions representing real numbers, which are built from the integers by using the arithmetical operations, the logarithm and the exponential ([[Richardson's theorem]]).