Semantics: Difference between revisions

Semantics (view source)

Revision as of 22:53, 15 March 2023

629 bytes added , 22:53, 15 March 2023

Finish explaining lambdas

Loekıa

Interface administrators

160

edits

@@ Line 47: / Line 47: @@
 ** <math>t,\ t',\ t'',\ \dots</math> for time intervals
 * <math>w,\ w',\ w'',\ \dots</math> for worlds
+* <math>P,\ Q,\ R,\ \dots</math> for functions (the exact type is left to context)
-It turns out we don't need variables for truth values or functions, so we don't assign them any.
+It turns out we don't need variables for truth values, so we don't assign them any.
-What this language does have though, is a special syntax for writing functions, known as a '''lambda expression'''. They're easy to spot because they start with the Greek letter <math>\lambda</math>, and have two components: a variable name representing the function's input, and an expression representing the function's output. For example, <math>\lambda n.\ 2n + 1</math> is a function that takes a value <math>n</math> as its input, and outputs the value <math>2n + 1</math>. Since <math>n</math> is a variable of type <math>\text{e}</math>, and <math>2n + 1</math> is an expression of type <math>\text{e}</math>, we can tell that this function has type <math>\left\langle e, e \right\rangle</math>. Similarly, <math>\lambda e.\ \text{saqsu}(\text{j}\mathrm{\acute{i}})(e)</math> is a function of type …
+Another important feature of this language is that it has a special syntax for writing functions, known as a '''lambda expression'''. They're easy to spot because they start with the Greek letter <math>\lambda</math>, and have two components: a variable name representing the function's input, and an expression representing the function's output. For example, <math>\lambda n.\ 2n + 1</math> is a function that takes a value <math>n</math> as its input, and outputs the value <math>2n + 1</math>. Since <math>n</math> is a variable of type <math>\text{e}</math>, and <math>2n + 1</math> is an expression of type <math>\text{e}</math>, we can tell that this function has type <math>\left\langle e, e \right\rangle</math>. Similarly, <math>\lambda e.\ \text{saqsu}(\text{j}\mathrm{\acute{i}})(e)</math> is a function of type <math>\left\langle \text{v}, \text{t} \right\rangle</math> which computes whether <math>e</math> is an event of the speaker whispering.
-TODO: finish lambdas
+You can apply these lambda functions to an argument in the same way you would apply a named function: by placing them before their argument, surrounded with parentheses. For example, if we say that <math>P</math> is the function <math>\lambda x.\ \text{ruq}(x)</math>, then <math>P(r)</math> and <math>(\lambda x.\ \text{ruq}(x))(r)</math> are two ways of saying the same thing—they both evaluate to <math>\text{ruq}(r)</math>.
 == Events ==