Lecture 6: Environments and Scoping

목차

Learning Objectives

- Explain what a "law" is

- Explain how to verify that a programming language interpreter satisfies a law

- Explain laws that uniquely characterize (simply-typed) functions

 

 

What is a "Law"?

An abstraction can be understood and defined independently of its underlying implementation

Abstract definition = syntax + laws

A law is an equation between two terms

 

Example:

→ 왼쪽이 Syntax, 오른쪽이 Law

 

a, b are valid expressions, i.e. well-formed according to <expr>

The values resulting from evaluating each expression is the same

(+  a  b)  =  (+  b  a)

 

 

Verifying that an Interpreter Satisfies a Law

How to verify that Law on the Right is Satisfied?

 

Approach 1: Write good tests

Approach 2: Generate tests and use property-based testing

Approach 3: Formally verify the law

 

 

 

With plus constructors, I unfold the definitions 

 

 

Towards Functions: Let Expressions

Syntax of a Language with Let Expressions

 

 

Intuition for let: A substitution

 

→ (let  (x  a)  y)  =  y. 이거는 let x = a, and y? = y

4. 

 

 

Should this law hold?

 

Wrong with scopes: Allows for name capturing when x and y bind to same name

원래는 x = 2이어야 함 (refer to its closest binding). 근데 오른쪽에 있는 law로 하면 x = 1이 됨 (Violates name shadowing policy).

The law does not hold

 

The law holds only if x ≠ y. Otherwise, wrong name shadowing

 

 

Renaming

 

 

 

 

Functions and Laws

Syntax of a Language with Functions

 

 

Example: