160
edits
Semantics: Difference between revisions
Progress on the propositions section, mostly
(Finish explaining lambdas) |
(Progress on the propositions section, mostly) |
||
| Line 51: | Line 51: | ||
It turns out we don't need variables for truth values, 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. | ||
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. | Be careful when reading these letters, because italics are meaningful. There are some tricky pairs of symbols such as <math>w</math>, which is a world variable, versus <math>\text{w}</math>, which is a constant referring to the real world, and <math>t</math>, which is a time interval variable, versus <math>\text{t}</math>, which is a constant referring to the salient time interval. | ||
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 \text{e}, \text{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. | |||
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>. | 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 == | ||
TODO don't forget to explain <math>\tau</math> | |||
== Worlds == | == Worlds == | ||
| Line 62: | Line 65: | ||
== Propositions == | == Propositions == | ||
A '''proposition''' is, in the broadest sense, anything that bears a truth value, such as a fact, a belief, or the meaning of a sentence. We can say that the sentence "The Earth is a planet" expresses the proposition that the Earth is a planet, and likewise, in the sentence "I believe that I saw a ghost", we can identify "that I saw a ghost" as referring to the proposition that the speaker saw a ghost. | |||
In Toaq, we can use the complementizer {{Derani||ꝡä}} to create a reference to a proposition, which can then become the complement of another verb. So, our semantic theory needs to account for this construct, and it turns out that it's best to use two different "implementations" of propositions for this purpose. | |||
The first implementation is '''propositions as functions'''. The idea is to interpret a complementizer phrase as a function which takes a world as an input, and outputs whether the proposition is true in that world (type <math>\left\langle \text{w}, \text{t} \right\rangle</math>). So for example, in {{Derani| |Chı jí, ꝡä za ruqshua}}, we would interpret the complementizer phrase as <math>\lambda w.\ \exists e.\ \tau(e) > \text{t} \land \text{ruqshua}_w(e)</math>, and pass this as an argument to the main verb, giving: <math>\exists e.\ \tau(e) \subseteq t \land \text{chi}_{\text{w}}(\text{ji}, \lambda w.\ \exists e'.\ \tau(e') > \text{t} \land \text{ruqshua}_w(e'))(e)</math> | |||
TODO: finish | |||
== Properties == | == Properties == | ||