X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week4.mdwn;h=8714eae88f924c42f7ba6560530d3094be741f07;hp=6613fb407220e8beac7532e117cc902bb5834a81;hb=1efc447d2ee3caf685576ea5b6332e7bf48bd1f3;hpb=9b65b6793ba00e0b9f42a5851f0b5185623abae8 diff --git a/week4.mdwn b/week4.mdwn index 6613fb40..8714eae8 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -227,12 +227,12 @@ which is the smallest set such that σ, then the application `(M N)` has type τ. * If a variable `a` has type σ, and term `M` has type τ, - then the abstract `λ a M` has type `σ --> τ`. + then the abstract λ a M has type σ --> τ. The definitions of types and of typed terms should be highly familiar -to semanticists, except that instead of writing `σ --> τ`, -linguists (following Montague, who followed Church) write `<σ, -τ>`. We will use the arrow notation, since it is more iconic. +to semanticists, except that instead of writing σ --> τ, +linguists (following Montague, who followed Church) write <σ, +τ>. We will use the arrow notation, since it is more iconic. Some examples (assume that `x` has type `o`):