Help with derivations

The derivation loop

A derivation is a tree computed bottom-up. Leaves take their meanings from the lexicon in the right panel. For every other node, the loop is: click a node whose children are resolved → choose a composition rule → type the β-reduced result → submit. A ✓ appears when your answer matches the target meaning. The whole loop also works by keyboard: Tab to a node, Enter or Space to select it.

Finding your way

The sidebar (left) is the map: Worksheets holds the built-in library — grouped by book (a Coppock & Champollion and a Heim & Kratzer family open to their chapters, with Classic papers alongside) — plus any class you unlock with a code. Continue returns to recently opened exercises, and Guide & help opens these help pages inside the app. ⌘K (Ctrl+K) opens a palette that searches worksheets, the current worksheet’s exercises, pages and actions; J/K step to the previous/next exercise. Right-clicking a worksheet or chapter row in the sidebar opens a small menu with its share code, QR & link, and (for worksheets) Copy to editor. On a tablet the stage is full-width: a ☰ button opens the navigation as a left drawer and a Reference button opens the Lexicon/Rules/Notes tabs as a right drawer. On a phone the same content lives in the bottom tab bar — Derive, Exercises, Reference, Menu: the worksheet switcher (tap the worksheet title on the Derive tab, or Menu → Switch worksheet) groups the library by book exactly like the sidebar, with a search box on top, and the foot of the Exercises tab shows the open worksheet’s Code · … and QR & link rows.

Unlock codes

A six-character code word adds a worksheet set to your sidebar. Enter it under ⊕ Unlock with a code (in the sidebar, the tablet navigation drawer, or the phone’s Menu tab) — or open a link like compose.tstephen.com/?code=ABCDEF, which is what the QR codes your instructor projects encode; both do the same thing. Codes come in two kinds. Library codes unlock built-in material — a single worksheet, a chapter, or a whole collection — and work without any account: the content opens right away and the set stays under Unlocked in your sidebar (the ✕ beside it removes it again; the code always works again later). Every open worksheet shows its own code and QR at the foot of the exercise list (Code · … and QR & link). Class codes come from your instructor's hosted material; those ask you to sign in first, land under My classes, and your progress in them syncs to your account.

The composition rules

A worksheet enables only the rules it needs; the Rules tab of the right-hand reference panel lists the ones active in the current worksheet, with a usage note each.

Rule	Applies when	Result
FA — Function Application	One sister has type ⟨σ,τ⟩ and the other has type σ.	The function applied to the argument, β-reduced.
NN — Non-branching Node	The node has exactly one child.	The child's meaning, unchanged.
PM — Predicate Modification	Both sisters are predicates ⟨σ,t⟩ of the same type σ.	λx[P(x) ∧ Q(x)] — the conjunction of the two predicates.
PA — Predicate Abstraction	One child is a bare index n and its sister is a resolved subtree.	λ-abstraction over the trace variable xₙ.
IFA — Intensional FA	One sister has type ⟨⟨s,σ⟩,τ⟩ and the other has type σ.	The function applied to λw.argument — abstraction over the evaluation world.
QR — Quantifier Raising	Enabled per worksheet; drag or select a quantifier phrase.	The phrase moves up, leaving an indexed trace bound by PA.

Type-shifts

Where a worksheet enables them, type-shifts apply to a single resolved node and change its type. The ones used across the built-in library:

Shift	Type	Term
Lift	e → ⟨⟨e,t⟩,t⟩	λx.λP.P(x)
Ident	e → ⟨e,t⟩	λx.λy.y = x
Iota (the)	⟨e,t⟩ → e	λP.ιz.P(z)
A	⟨e,t⟩ → ⟨⟨e,t⟩,t⟩	λP.λQ.∃z[P(z) ∧ Q(z)]
BE	⟨⟨e,t⟩,t⟩ → ⟨e,t⟩	λT.λx.T(λy.y = x)
Lower	⟨⟨e,t⟩,t⟩ → e	λT.ιz.T(λy.z = y)
MOD / PRED	⟨e,t⟩ ↔ ⟨⟨e,t⟩,⟨e,t⟩⟩	attributive ↔ predicative adjectives
EC	⟨τ,σ⟩ → σ	existential closure over individuals, events or times

The first six are Partee's (1986) NP-shifting inventory; MOD/PRED and EC follow Coppock & Champollion (2022).

Typing answers

Answers are typed in plain ASCII; the input converts as you type:

You type	You get
Lx.	λx.
Ax[…] / Ex[…] / Ix[…]	∀x[…] / ∃x[…] / ιx[…]
&	∧
~	¬
->	→

The clickable symbol palette under the input covers everything else, and it shows only the operator symbols the current worksheet uses — a worksheet without mereology shows no ∗ ⊕ ≤ keys.

How grading works

Grading is by meaning, not spelling. Your answer is parsed, normalized, and compared with the target up to renaming of bound variables (α-equivalence); the order of conjuncts does not matter, so Lx.[cat(x) & grey(x)] and Lx.[grey(x) & cat(x)] are the same answer. What does matter is that you actually perform the β-reduction: an unreduced function–argument application is not accepted as the value of the node you are computing, because the reduction is the exercise.

Reading the feedback

Choosing an inapplicable rule is refused with the type-theoretic reason — for example: "Both sisters must be predicates ⟨A,t⟩ of the same type A. The sisters are ⟨e,⟨e,t⟩⟩ and e." That message tells you the two types the rule saw; compare them against the rule's condition in the table above. A near-miss answer gets a hint such as "Not equivalent yet — check which variable each argument replaces": re-do the substitution slowly, one λ at a time, outermost first.

Progress & hints

Where the author provided them, derivations carry staged hints, revealed one at a time; the final stage offers "Show answer" unless the worksheet's version is set up as an assessment. The Notes tab of the reference panel holds the worksheet's reading companion, and opening an exercise scrolls it to its section. Progress is stored in your browser; the sidebar's Your progress page shows per-worksheet counts and has "Save to a file" / "Restore" for moving it between machines — and a signed-in student's progress also syncs to their account.

Questions that this page doesn't answer are usually answered by the worksheet's own Notes tab or the worked derivation guides. Instructors: see the instructor guide.