From: Chris Barker Date: Sun, 3 Oct 2010 01:01:20 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=f4e64dfd73d6935c7636a1f4586b7d5202a74272;hp=3af15277e1a4116c0eb3025f371e0a9a9417ebc9 edits --- diff --git a/week4.mdwn b/week4.mdwn index 1f52cf3b..8714eae8 100644 --- a/week4.mdwn +++ b/week4.mdwn @@ -217,7 +217,7 @@ and so on. #Typed lambda terms# -Given a set of types `T`, we define the set of typed lambda terms Λ~T~, +Given a set of types `T`, we define the set of typed lambda terms Λ_T, which is the smallest set such that * each type `t` has an infinite set of distinct variables, {x^t}_1, @@ -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`):