Exploring Concepts in Functional Programming and Grammar Analysis

PL Summary Yotam Feldman Mooly Sagiv

Concepts &Techniques Functional programming Lambda calculus Recursion Higher order programming Lazy vs. Eager evaluation Continuation Pattern matching Closure Types Type safety Static vs. dynamic Type checking vs. type inference Most general type Polymorphism Type inference algorithm Mathematical Induction Syntax Context free grammar Ambiguous grammars Syntax vs. semantics Static semantics Scope rules Type Rules Semantics Small vs. big step Runtime management Activation records GC

Languages Ocaml Javascript

Types of Context Free Grammars Linear Grammars Non-Ambiguous Grammars

Example Languages a* (a | b)* anbn Regular expressions over letters, +, ., *, (, ) w c w w c wr

What do I have to know about grammars Define programming language constructs Ambiguity

Static Semantics Context Analysis

Semantic Analysis Properties which are not enforced by the grammar Every used identifier is previously defined The type of the arguments match the type of the function prototype

Static Scope Rules Modern programming languages provide two ways to open new scopes Inline blocks Functions C like syntax { } Ocaml like syntax let x = 5 in x + 7

C like void main { int x=1; int g(z) { return x+z; } int f(y) { int x = y+1; return g(y*x); } f(3); g(4);

Javascript var x=1; function g(z) { return x+z; } function f(y) { var x = y+1; return g(y*x); } f(3); g(4);

Ocaml let x = 1 in let rec g z = x + z and f y = let x = y + 1 in g (y * x) in f 3 , g 4

Ocaml Emphasis Algebraic data types Higher order functions and recursion Closures Modules

Type Checking and Type Inference Statically typed languages permit effective compile time checking of types Proves type-safety Identify subtle interface mismatch Type inference Automatically infer the most general type for a given expression

Most General Type Examples fun f x = let val a = x * 2 and val b = x * 3 in [0, x, a, b, x * 4] rec fun f x = match x with [] 0 | h :: t 1 + f t rec fun f x = match x with [] 0 | h :: t 1 rec fun f x = match x with [] [0] | h :: t 1

Type Inference Algorithm Parse program to build parse tree Assign type variables to nodes in tree Generate constraints: From environment: literals (2), built-in operators (+), known functions (tail) From form of parse tree: e.g., application and abstraction nodes Solve constraints using unification Determine types of top-level declarations

Alternative Formal Semantics Operational Semantics The meaning of the program is described operationally Natural Operational Semantics Structural Operational Semantics Denotational Semantics The meaning of the program is an input/output relation Mathematically challenging but complicated Axiomatic Semantics The meaning of the program are observed properties

The While Programming Language Abstract syntax S::= x := a | skip | S1 ; S2| if b then S1else S2| while b do S Use parenthesizes for precedence Informal Semantics skip behaves like no-operation Import meaning of arithmetic and Boolean operations

General Notations Syntactic categories Var the set of program variables Aexp the set of arithmetic expressions Bexp the set of Boolean expressions Stm set of program statements Semantic categories Natural values N={0, 1, 2, } Truth values T={ff, tt} States State = Var N Lookup in a state s: s x Update of a state s: s [ x 5]

Example State Manipulations [x 1, y 7, z 16] y = [x 1, y 7, z 16] t = [x 1, y 7, z 16][x 5] = [x 1, y 7, z 16][x 5] x = [x 1, y 7, z 16][x 5] y =

Semantics of arithmetic expressions Assume that arithmetic expressions are side-effect free A Aexp : State N Defined by structural induction on the syntax tree A n s = n A x s = s x A e1+ e2 s = A e1 s + A e2 A e1* e2 s = A e1 s * A e2 A ( e1) s = A e1 s --- not needed A - e1 s = -A e1 s s s

OCaml Code type exp = Id of string | Number of int | Plus of exp * exp let rec interpret s = function Number(v) -> v | Id(var) -> match find s var with None -> assert false | Some(v) -> v | Plus(v1, v2) -> interpret s v1 + interpret s v2

Natural Semantics for While [assns] <x := a, s> s[x A a s] [skipns] <skip, s> s [whileffns] <while b do S, s> s axioms if B b s=ff <S1, s> s , <S2, s > s <S1; S2, s> s <S1, s> s <if b then S1 else S2, s> s [compns] rules [ifttns] if B b s=tt <S2, s> s <if b then S1 else S2, s> s [ifffns] if B b s=ff <S , s> s , <while b do S, s > s <while b do S, s> s [whilettns] if B b s=tt

An Example Derivation Tree <(x :=x+1; y :=x+1) ; z := y), s0> s0[x 1][y 2][z 2] compns <x :=x+1; y :=x+1, s0> s0[x 1][y 2] compns <z :=y,s0[x 1][y 2]> s0[x 1][y 2][z 2] assns <x :=x+1; s0> s0[x 1] <y :=x+1, s0[x 1]> s0[x 1][y 2] assns assns

Top Down Evaluation of Derivation Trees Given a program S and an input state s Find an output state s such that <S, s> s Start with the root and repeatedly apply rules until the axioms are reached Inspect different alternatives in order In While s and the derivation tree is unique

OCaml Statement Type type St = Skip | Assign of string * exp | Seq of St * St | If of Cond * St * St | While of Cond * St

OCaml NS Interpreter let rec ns_interpret s st = match st with Skip -> s | Assign(var, ex) -> add s var (interpret s ex) | Seq(st1, st2) -> ns_interpret (ns_interpret s st1) st2 | If (cond, st1, st2) -> let b = c_interpret s cond in if b then ns_interpret s st1 else ns_interpret s st2 | While(cond, body) -> let b = c_interpret s cond in if b then ns_interpret (ns_interpret s body) st else s

Semantic Equivalence S1and S2 are semantically equivalent if for all s and s <S1, s> s if and only if <S2, s> s Simple example while b do S is semantically equivalent to: if b then (S ; while b do S) else skip

Deterministic Semantics for While If <S, s> s1and <S, s> s2then s1=s2 The proof uses induction on the shape of derivation trees Prove that the property holds for all simple derivation trees by showing it holds for axioms Prove that the property holds for all composite trees: For each rule assume that the property holds for its premises (induction hypothesis) and prove it holds for the conclusion of the rule

The Semantic Function Sns The meaning of a statement S is defined as a partial function from State to State Sns: Stm (State State) SnsS s = s if <S, s> s and otherwise SnsS s is undefined Examples Snsskip s =s Snsx :=1 s = s [x 1] Snswhile true do skip s = undefined

Structural Operational Semantics Emphasizes the individual execution steps <S, i> If the first step of executing the statement S on an input state i leads to Two possibilities for = <S , s > The execution of S is not completed, S is the remaining computation which need to be performed on s = o The execution of S has terminated with a final state o is a stuck configuration when there are no transitions The meaning of a program P on an input state s is the set of final states that can be executed in arbitrary finite steps

Structural Semantics for While [asssos] <x := a, s> s[x A a s] [skipsos] <skip, s> s [comp1sos] <S1, s> <S 1, s > <S1; S2, s> < S 1; S2, s > axioms rules [comp2sos] <S1, s> s <S1; S2, s> < S2, s >

Structural Semantics for While if construct [ifttsos] <if b then S1 else S2, s> <S1, s> if B b s=tt [ifffos] <if b then S1 else S2, s> <S2, s> if B b s=ff

Structural Semantics for While while construct [whilesos] <while b do S, s> <if b then (S; while b do S) else skip, s>

Structural Semantics for While (Summary) [asssos] <x := a, s> s[x A a s] [skipsos] <skip, s> s [ifttsos] <if b then S1 else S2, s> <S1, s> [ifffsos] <if b then S1 else S2, s> <S2, s> [whilesos] <while b do S, s> <if b then (S; while b do S) else skip, s> axioms if B b s=tt if B b s=ff rules [comp1sos] <S1, s> <S 1, s > <S1; S2, s> < S 1; S2, s > [comp2sos] <S1, s> s <S1; S2, s> < S2, s >

Example S=[x S = (z:=x; x := y); y := z 5 , y 7] (z:=x; x := y); y := z, [x 5, y 7] => x := y ; y := z, [x 5, y 7, z 5] comp1sos z:= x; x := y , [x 5, y 7] => x := y ; y := z, [x 5, y 7, z 5] comp2sos asssos z:= x , [x 5, y 7] => [x 5, y 7, z 5]

Example (2ndstep) S=[x S = (z:=x; x := y); y := z 5 , y 7] x := y; y := z, [x 5, y 7, z 5] => y := z, [x 7, y 7, z 5] comp2sos x := y , [x 5, y 7, z 5] => x := y ; y := z, [x 7, y 7, z 5] asssos

Example (3rdstep) S=[x S = (z:=x; x := y); y := z 5 , y 7] y := z [x 7, y 7, z 5] => y := z, [x 7, y 5, z 5] asssos

Factorial Program Input state s such that s x = 3 y := 1; while (x=1) do (y := y * x; x := x - 1) <y :=1 ; W, s> <W, s[y 1]> <if (x =1) then (y := y * x ; x := x 1 else skip); W), s[y 1]> < ((y := y * x ; x := x 1); W), s[y 1]> <(x := x 1 ; W), s[y 3]> < W , s[y 3][x 2]> <if (x =1) then ((y := y * x ; x := x 1); W) else skip, s[y 3][x 2]> < ((y := y * x ; x := x 1); W), s[y 3] [x 2] > <(x := x 1 ; W) , s[y 6] [x 2] > < W, s[y 6][x 1]> <if (x =1) then (y := y * x ; x := x 1); W) else skip, s[y 6][x 1]> <skip, s[y 6][x 1]> s[y 6][x 1]

Finite Derivation Sequences finite derivation sequence starting at <S, i> 0, 1, 2 , ksuch that 0=<S, i> i i+1 k is either stuck configuration or a final state For each step there is a derivation tree 0 k k in k steps 0 * in finite number of steps

Infinite Derivation Sequences An infinite derivation sequence starting at <S, i> 0, 1, 2 such that 0=<S, i> i i+1 Example S = while true do skip s0x = 0

Program Termination Given a statement S and input s S terminates on s if there exists a finite derivation sequence starting at <S, s> S terminates successfully on s if there exists a finite derivation sequence starting at <S, s> leading to a final state S loops on s if there exists an infinite derivation sequence starting at <S, s>

OCaml Types State Configurations type s Configuration = Atomic of s | Comp of St * s Configuration

OCaml SOS Interpreter let rec sos_interpret s st = match st with Skip -> Atomic(s) | Assign(var, ex) -> Atomic(add s var (interpret s ex)) | Seq(st1, st2) -> match sos_interpret s st1 with Atomic(s ) -> Comp(st2, s ) | Comp(st1 , s ) -> Comp(Seq(st1 , st2), s ) | If (cond, st1, st2) -> let b = c_interpret s cond in if b then Comp (st1, s) else Comp(st2, s) | While(cond, body) -> Comp(If(cond, Seq(body, st), Skip), s)

OCaml Interpreter let rec sos_interpret_star s st = match sos_interpret s st with Atomic(s ) -> s | Comp(st , s ) -> sos_interpret s st

Properties of the Semantics S1and S2 are semantically equivalent if: for all s and which is either final or stuck <S1, s> * if and only if <S2, s> * there is an infinite derivation sequence starting at <S1, s> if and only if there is an infinite derivation sequence starting at <S2, s> Deterministic If <S, s> *s1and <S, s> *s2then s1=s2 The execution of S1; S2on an input can be split into two parts: execute S1on s yielding a state s execute S2on s

Sequential Composition If <S1; S2, s> ks then there exists a state s and numbers k1and k2 such that <S1, s> k1s <S2, s > k2s and k = k1 + k2 The proof uses induction on the length of derivation sequences Prove that the property holds for all derivation sequences of length 0 Prove that the property holds for all other derivation sequences: Show that the property holds for sequences of length k+1 using the fact it holds on all sequences of length k (induction hypothesis)

The Semantic Function Ssos The meaning of a statement S is defined as a partial function from State to State Ssos: Stm (State State) SsosS s = s if <S, s> *s and otherwise SsosS s is undefined

An Equivalence Result For every statement S of the While language SnatS = SsosS

Extensions to While Abort statement (like C exit w/o return value) Non determinism Parallelism Local Variables Procedures Static Scope Dynamic scope