Go backward to Summary (Semantics) Go up to Top

Summary (Lambda Abstraction)

• Abstract syntax:
  • D ::= ...| define I₁ = A
    A ::= lambdaI:theta. U
    U ::= ...| invoke I(V)
    V ::= ...| I
• Typing rules:

  • pi -U- {I:theta1} |- E:theta2

    pi |- (lambdaI:theta1.E): theta1 -> theta2

• Semantics:
  • [[pi |-lambdaI:theta₁.E: theta₁ -> theta₂]]e = f
       where f v = [[pi -U- {I:theta₁} |- E:theta₂]](e -U- {I=v})
• Parameter copy rule:
  • (lambdaI:theta. U)V => [V/I]U