Go backward to Example Go up to Top Go forward to Example

Lambda Abstraction Introduction

• Parameterization principle:
  • E ::= ...| lambdaI:theta. E | E₁ E₂ | I

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

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

    
    

    pi |- E1: theta1 -> theta2	pi |- E2: theta1
    pi |- E1 E2: theta2

    
    

    pi |- I: theta

    if (I:theta) in pi
• Lambda abstraction lambdaI₂:theta. E
  • Abstraction invocation E₁ E₂
  • Parameter reference I.
• Correspondence principle
  • Semantics of definition binding and semantics of parameter binding is the same.
• Enrichement of type system
  • New attribute theta₁ -> theta₂