程序设计语言的形式语义

3 - Simply Typed Lambda Calculus

2019-10-18 10:00 CST
2019-11-01 12:00 CST
CC BY-NC 4.0

Adding Types

Adding types to $\lambda$-calculus:

  • Classify functions using argument and result types
  • Type-check function bodies, which have free variables

Simply-typed $\lambda$-calculus (STLC):

Suppose T is base types (int, bool, etc.),

$$\text{(Types) } \tau, \sigma ::= \text{T} \ \vert \ \tau \rightarrow \sigma$$

$\rightarrow$ is right-associative.

Typing Judgement

Judgement: A statement $J$ about certain formal properties

  • Has a derivation (proof): $\vdash J$
  • Has a meaning (judgement semantics): $\vDash J$

$\Gamma \vdash M:\tau$ ($M$ is of type $\tau$ in context $\Gamma$)

  • Typing context (a set of typing assumptions)
    • $\Gamma ::= \cdot \ \vert \ \Gamma, x:\tau$
    • Includes types of all the free variables in $M$
    • Empty context $\cdot$ is for closed terms
  • Under $\Gamma$, $M$ is a well-typed term of type $\tau$.

Typing Rules

  • var: $${ \over \Gamma, x:\tau \vdash x:\tau}$$
  • app: $${\Gamma \vdash M:\sigma\rightarrow\tau \ \ \ \ \ \ \Gamma \vdash N:\sigma \over \Gamma \vdash MN:\tau}$$
  • abs: $${\Gamma, x:\sigma \vdash M:\tau \over \Gamma \vdash (\lambda x:\sigma . M):\sigma\rightarrow\tau}$$

Soundness and Completeness

  • A sound type system never accepts a program that can go wrong
    • No false negatives
    • The langauge is type-safe
  • A complete type system never rejects a program that cannot go wrong
    • No false positives
  • However, for any Turing-complete PL, the set of programs that may go wrong is undecidable
    • Type system cannot be sound and complete
    • Choose soundness, try to reduce false positives in practice

Soundness

Theorem (Type Safety):

If $\cdot \vdash M:\tau$ and $M \rightarrow^* M'$, then $\cdot \vdash M':\tau$, and either $M' \in \text{Values}$ or $\exists M'', M' \rightarrow M''$

(the reduction of a well-typed term either diverges, or terminates in a value of the expected type)

  • Preservation (subject reduction): well-typed terms reduce only to well-typed terms of the same type
    • If $\cdot \vdash M:\tau$ and $M \rightarrow M'$, then $\cdot \vdash M':\tau$
  • Progress: a well-typed term is either a value or can be reduced
    • If $\cdot \vdash M:\tau$, then either $M' \in \text{Values}$ or $\exists M'', M' \rightarrow M''$

Not Complete

The type system may reject terms that do not go wrong.

E.g. $(\lambda x.(x(\lambda y.y)) (x \ 3)) (\lambda z.z)$

  • Cannot find $\sigma, \tau$ that $x:\sigma \vdash (x (\lambda y.y))(x \ 3) : \tau$ because we have to pick one type for $x$.
  • But the term equals to 3.

Strong Normalization Theorem

Well-typed terms in STLC always terminate.

Adding Stuff

Product Type

Structures in C $\Leftrightarrow$ Products

  • (Types) $\tau, \sigma ::= \dots \ \vert \ \sigma \times \tau$
  • (Terms) $M, N ::= \dots \ \vert \ < M , N > \ \vert \ \text{proj1 } M \ \vert \ \text{proj2 } M$

Typing rules:

  • pair $${\Gamma \vdash M:\sigma \ \ \ \ \Gamma \vdash N:\tau \over \Gamma \vdash < M , N >:\sigma\times\tau}$$
  • proj1 $${\Gamma \vdash M:\sigma\times\tau \over \Gamma \vdash \text{proj1 }M:\sigma}$$
  • proj2 $${\Gamma \vdash M:\sigma\times\tau \over \Gamma \vdash \text{proj2 }M:\tau}$$

Sum Type

Unions in C, Subclasses in Java $\Leftrightarrow$ Sums

  • (Types) $\tau, \sigma ::= \dots \ \vert \ \sigma + \tau$
  • (Terms) $M, N ::= \dots \ \vert \ \text{left } M \ \vert \ \text{right } M \ \vert \ \text{case } M \text{ do } M1 \ M2$

case ... do ...: if $M$ is of type $\sigma$ then $M1$, otherwise $M2$

Products vs. Sums

  • Logical duals
    • To make a $\sigma \times \tau$, we need a $\sigma$ and a $\tau$
    • To make a $\sigma + \tau$, we need a $\sigma$ or a $\tau$
    • Given a $\sigma \times \tau$, we can get a $\sigma$ or a $\tau$ or both (our choice)
    • Given a $\sigma + \tau$, we must be prepared for either a $\sigma$ or a $\tau$ (the value’s choice)

Recursion

Recall: Fixpoint combinator in untyped $\lambda$-calculus

Strong normalization theorem: well-typed terms in STLC always terminate.

However, recursion is not allowed by the typing rules (there is no types for fixed-point combinators).

Therefore we need an explicit construct for recursion: define a new type $\textbf{fix } M$ in terms.

Reduction rules for fix:

$${ \over \textbf{fix } \lambda x.\ M \rightarrow M[\textbf{fix } \lambda x.\ M / x]}$$

$${M \rightarrow M' \over \textbf{fix } M \rightarrow \textbf{fix } M'}$$

Typing rule for fix:

$${\Gamma \vdash M : \tau \rightarrow \tau \over \Gamma \vdash \textbf{fix } M : \tau}\ (\text{fix})$$

Curry-Howard Isomorphism

What we did:

  • Programming language
  • A type system to rule out “bad” programs

What logicians do:

  • Define logic propositions
  • Defina a proof system to prove “good” propositions

Isomorphism (Slogan):

  • Propositions are Types
    • Propositions: $\text{boolean} \vert p \Rightarrow q \vert p \wedge q \vert p \vee q$
    • Types: $\text{T} \vert \sigma \rightarrow \tau \vert \sigma \times \tau \vert \sigma + \tau$
  • Proofs are Programs

Different types:

Types Examples

  • Nonempty types: closed terms of that type
  • Empty types: non closed terms of that type
  • How do we know whether a type is empty?
    • Replace $\rightarrow$ with $\Rightarrow$, $\times$ with $\wedge$, $+$ with $\vee$
    • Nonempty types can be proved in propositional logic
    • Empty types cannot be proved in propositional logic

Propositional Logic

Isomorphismed Logic

Curry-Howard Isomorphism:

  • Given a well-typed closed term, take the typing derivation, erase the terms, and have a propositional-logic proof
  • Gien a propositional-logic proof, there exists a closed term with that type
  • A term that type-checks is a proof
  • Constructive propositional logic and STLC with pairs and sums are the same thing

Classical v.s. Constructive

Law of the ecluded middle: $${\over \Gamma \vdash p \vee (p \Rightarrow q)}$$

STLC does not support it: no closed term has type $\rho + (\rho \rightarrow \sigma)$.

Logics without this rule are called “constructive” or “intuitionistic”. Formulas are only considered “true” when we have direct evidence.

Classical Proof

Transform to constructive logic: if any number is either rational or irrational, then there exists two irrational numbers …

A valid proof must terminate, however the reduction of $\textbf{fix}$ does not terminate. Thus including $\textbf{fix}$ would make the logic inconsistent.