The lambda calculus (simply typed)

BasType is a subset of Typ
BasType = {e, t, s, w, ...} (Entities, Truth Values, Situations, Possible Worlds)
sigma, tau in Typ => sigma -> tau in Typ

Term_tau:
- Var_tau in Term_tau (Variables)
- Con_tau in Term_tau (Constants)
- alpha in Term_{sigma -> tau}, beta in Term_sigma => alpha(beta) in Term_tau (Application)
- x in Var_sigma, beta in Term_tau => lambda x . beta in Term_{sigma -> tau} (Abstraction)

Term = Union_{tau in Typ] Term_tau

Note: We do not specify boolean connectives but instead put and, or and => (implication) in Con_{t x t -> t}

Comp_<sigma, tau, roe> "is congruent to" lambda g_{tau -> roe} . lambda f_{sigma -> roe} . lambda x_sigma . g(f(x))

Curry-Howard Isomorphism
- An alternative to model-theoretic proof theory

Frames:
<Dom, || . ||_M> = M
Dom = Union_{tau in BasTyp} Dom_tau
Dom_{alpha -> beta} "is congruent to" Dom^{Dom_alpha}_beta

Variable interpretation function:
theta: Var -> Dom
x in Var_tau => theta(x) in Dom_tau

|| alpha ||^theta_M 
= theta(x) if alpha = x in Var_tau
= ||c||_M if alpha = c in Con_tau
= ||beta||^theta_M(||gamma||^theta_M) if alpha = beta(gamma)
= f s.t. for every alpha in Dom(theta) f(a) = ||beta||^{theta[x |-> a]}_M if alpha = lambda x . beta

Theorem(Soundness): If alpha in Term_tau, then ||alpha||^theta_M in Dom_tau for every M, theta

Definition: alpha "is congruent to" beta iff ||alpha||^theta_M = ||beta||^theta_M for every theta, M

Note: The relationship between frames and the lambda calculus here is one such that frames provide a semantics for the lambda calculus

Definition: alpha free for x in beta iff one of the following is true
- beta in Con or Var
- beta = gamma(delta) where alpha free for x in gamma or alpha free for x in delta
- beta = lambda y . gamma where alpha free for x in gamma and either x is not in Free(gamma) or y not in Free(alpha)

Intuitively, this definition means that substituting alpha for x means that nothing bad will happen

The axioms and inference rules of the calculus

---------------------------------------------------------------- (alpha-conversion)
lambda x . beta => lambda y . beta[ x |-> y ] (y free for x in alpha)
  - here, the => is referred to as "evaluates to"

---------------------------------------------------------------- (beta-reduction)
(lambda x . alpha)(beta) => alpha[x |-> beta] (beta free for x in alpha)
  - in reverse, this is referred to as beta-expansion

------------------------------------------- (eta-reduction)
lambda x . [alpha(x)] => alpha (x not in Free(alpha))
  - in reverse, this is referred to as eta-expansion
  - here, the []'s only delineate scope

----------------------(reflexivity)
alpha => alpha


alpha => beta   beta => gamma
---------------------------------------------- (transitivity)
            alpha => gamma

alpha => gamma   beta => gamma
-------------------------------------------------- (equivalence)
            alpha <=> beta

alpha => beta   beta => alpha
------------------------------------------- (symmetric closure)
            alpha <=> beta

alpha => alpha'   beta => beta'
-------------------------------------------- (congruence1)
   alpha(beta) => alpha'(beta')

                 alpha => alpha'
------------------------------------------------------- (congruence2)
lambda x . alpha => lambda x . alpha'

Definition: beta =_alpha gamma if and only if beta reduces to alpha using only alpha-conversion and the two congruence rules

Theorem (Soundness): If alpha => beta, then alpha "is congruent to" beta

Theorem (Church-Rosser): If alpha => beta and alpha => gamma then there is delta s.t. beta => delta and gamma => delta

Theorem (Strong Normalization): Given a sequence beta_1, beta_2, ... there is a least j such that either it is not the case that beta_j => beta_{j+1} or beta_j can be converted to beta_{j+1} via alpha-conversions, congruence1 or congruence2's

These theorems give us that for every lambda term, there is one normal form (subject to alpha-conversions and congruences).

Definition: In case of beta_1, beta_2, ... reduction terminates at beta_j

Definition: A lambda term alpha is in beta-eta-normal form if and only if there is no subterm gamma of alpha s.t. gamma =_alpha gamma' and gamma' is a beta-redex or an eta-redex (where a beta-redex is something of the form (lambda x . alpha)(beta) for some x, alpha and beta and an eta-redex is something of the form lambda x . [alpha(x)] for some alpha and x)

Definition: A lambda term alpha is beta-eta-long form if and only if for every subterm gamma of alpha:

1) gamma_{sigma -> tau} and is applied to an argument or gamma = lambda x . beta and

2) there is no gamma' =_alpha gamma s.t. gamma' is a beta-redex

Note: This definition requires for all of the beta and eta reductions to beta-eta-normal form and then one eta expansion back.

Example:

beta-eta-normal form: run
beta-eta-long form: lambda x . run(x)

beta-eta-normal form: every(boy)(run)
beta-eta-long form: every(lambda x . boy(x))(lambda x . run(x))

Theorem (Completeness): alpha "is congruent to" beta if and only if alpha <=> beta

Untyped lambda calculus
- Exactly the same as the simply typed lambda calculus except with no types
- This allows for function application to happen on objects that aren't functions
- We still get the Church-Rosser property, a weaker Normalization result, Soundness and Completeness, but not strong normalization

Example: (lambda x . alpha) (beta)

Call-by-value:
                            beta => beta'
--------------------------------------------------------------------------- (congruence_2)
(lambda x . alpha)(beta) => (lambda x . alpha)(beta')
---------------------------------------------------------------------------(beta-reduction)

Call-by-name:
-------------------------------- (beta-reduction)
(lambda x . alpha)(beta) => alpha[x|-> beta]

                            beta => beta'
--------------------------------------------------------------- (congruence)
           alpha[x |-> beta] => alpha[x |-> beta']
--------------------------------------------------------------- (transitivity)
(lambda x . alpha)(beta) => alpha[x |-> beta']

Let w = lambda x . x (x) (x)
Now consider (lambda y . lambda z . z) (w (w))

Call-by-name: lambda z . z
Call-by-value: w (w) = (lambda x . x (x) (x)) (lambda x . x (x) (x)) => (lambda x . x (x) (x)) (lambda x . x (x) (x)) (lambda x . x (x) (x)) => ...

So, the completeness theorem does not hold