Semantics: Difference between revisions

629 bytes added ,  22:53, 15 March 2023
Finish explaining lambdas
(Save my half-finished explanation of lambdas)
(Finish explaining lambdas)
Line 47: Line 47:
** <math>t,\ t',\ t'',\ \dots</math> for time intervals
** <math>t,\ t',\ t'',\ \dots</math> for time intervals
* <math>w,\ w',\ w'',\ \dots</math> for worlds
* <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 ==
== Events ==