Derivation guides

Worked, step-by-step walkthroughs of three derivations, from the demo worksheet to Predicate Modification. The rule reference lives at Help with derivations.

1 · "Frodo runs" — your first derivation

Open the demo worksheet. The tree is [S [DP Frodo] [VP runs]]; the lexicon gives ⟦Frodo⟧ = f (type e) and ⟦runs⟧ = λx.run(x) (type ⟨e,t⟩).

  1. Click the VP node. It has one child, runs, so the only rule that fits is NN — the leaf's meaning λx.run(x) passes up unchanged.
  2. Click the DP node and choose NN again: it receives f.
  3. Click the S node. Its two daughters are now resolved. Their types are ⟨e,t⟩ and e — a function and its argument — so choose FA.
  4. Type the result. The application is (λx.run(x))(f); β-reduction substitutes f for x. Type run(f) and submit. ✓

If you instead type (Lx.run(x))(f), it is rejected: the unreduced application is not the computed value — performing the reduction is the exercise.

The whole derivation, as recorded in the app: NN on VP and DP, then FA at S and typing run(f).

2 · A transitive verb — "Frodo greets Gandalf"

Same worksheet, group B. The verb is ⟦greets⟧ = λx.λy.greet(y,x), type ⟨e,⟨e,t⟩⟩ — it takes the object first, then the subject. The tree is [S [DP Frodo] [VP [V greets] [DP Gandalf]]].

  1. Resolve the leaves (NN on the DPs and V as needed).
  2. VP node: ⟨e,⟨e,t⟩⟩ meets e → FA. The reduction is (λx.λy.greet(y,x))(g): substitute g for x only. Type Ly.greet(y,g).
  3. S node: ⟨e,t⟩ meets e → FA again. (λy.greet(y,g))(f) → greet(f,g). ✓

The common slip at the VP: substituting g for the wrong variable and typing λy.greet(g,y) — which says Gandalf greets y. The grader refuses it with the "check which variable each argument replaces" hint. The λ that gets the first argument is the outermost one.

Recorded end to end: switching to the exercise in the drill-in exercises column, then both FA steps — the object composes first (typing Ly.greet(y,g) at VP), then the subject at S.

3 · Predicate Modification — an adjective plus a noun

Open the §7 adjectives worksheet — enter its code MQ6GK7 under “⊕ Unlock with a code”, or just follow this link — and take the first derivation: Pippin is a mischievous hobbit. The interesting node is the inner NP: ⟦mischievous⟧ = λx.mischievous(x) and ⟦hobbit⟧ = λx.hobbit(x) are both ⟨e,t⟩. Neither can apply to the other, so FA is refused — try it and read the message. The rule that fits two same-typed predicates is PM, and the value to type is their conjunction:

Lx.[mischievous(x) & hobbit(x)]

Conjunct order doesn't matter — Lx.[hobbit(x) & mischievous(x)] is the same answer. The rest of the derivation is FA/NN as before.

The Rules tab of the reference panel lists what this worksheet allows; FA is then tried and refused with the type-theoretic reason, and PM conjoins the two ⟨e,t⟩ predicates.

When you're stuck

In rough order: (1) click the rule anyway — a refusal states the type-theoretic reason, which usually identifies the problem; (2) check the node's expected type against the lexicon entries below it; (3) open the reference panel's Notes tab — exercises are anchored to the section that introduces their construction; (4) use the staged hints where provided — the last hint offers “Show answer” unless the worksheet is set up as an assessment; (5) reset the derivation (↺) and rebuild bottom-up. The rule reference has the full rule and symbol tables.

Instructors: the instructor guide covers authoring, hosting and sharing. The full worksheet library is on /files.