7. Explain all the essentials of Types and Programming Languages operational semantics of Booleans, Figure 3-1, Arithmet
Posted: Wed Apr 27, 2022 3:29 pm
7. Explain all the essentials of Types and Programming
Languages operational semantics of Booleans, Figure 3-1, Arithmetic
expressions, Figure 3-2, Untyped lambda-calculus, Figure 5-3.
Provide illustrating examples of the usage of each of the
rules.
B (untyped) Syntax Evaluation t t' t if true then t2 else t3 --t2 (E-IFTRUE) true false ift then t else t terms: constant true constant false conditional if false then t2 else t3 = t3 (E-IFFALSE) (E-IF) ti — tí if ti then t2 else t3 niftſ then t2 else të values: true value false value true false Figure 3-1: Booleans (B)
B (untyped) Extends B (3-1) New syntactic forms New evaluation rules t-t' t HE 0 ti — succ ti — succ tí (E-SUCC) terms: constant zero successor predecessor zero test succt pred t iszerot pred 0 - 0 (E-PREDZERO) pred (succ nvı) - nv1 (E-PREDSUCC) V "= values: numeric value ην ti pred ti → ti pred t (E-PRED) ny = 0 succ nv numeric values: zero value successor value iszero 0 -- true (E-ISZEROZERO) iszero (succ nvı) - false (E-ISZEROSUCC) ti iszero ti ti iszerot (E-ISZERO) Figure 3-2: Arithmetic expressions (NB)
– (untyped) Syntax t Evaluation t-t' = Х terms: variable abstraction application ti — tí ti t2 — tít2 (E-APP1) ax.t tt t2 —- tz Vi t2 —— Vi t' (E-APP2) V values: abstraction value dx.t (Ax.t12) V2 -- [x - V2]t12 - (E-APPABS) Figure 5-3: Untyped lambda-calculus (4)
Languages operational semantics of Booleans, Figure 3-1, Arithmetic
expressions, Figure 3-2, Untyped lambda-calculus, Figure 5-3.
Provide illustrating examples of the usage of each of the
rules.
- 7 Explain All The Essentials Of Types And Programming Languages Operational Semantics Of Booleans Figure 3 1 Arithmet 1 (91.14 KiB) Viewed 30 times
B (untyped) Extends B (3-1) New syntactic forms New evaluation rules t-t' t HE 0 ti — succ ti — succ tí (E-SUCC) terms: constant zero successor predecessor zero test succt pred t iszerot pred 0 - 0 (E-PREDZERO) pred (succ nvı) - nv1 (E-PREDSUCC) V "= values: numeric value ην ti pred ti → ti pred t (E-PRED) ny = 0 succ nv numeric values: zero value successor value iszero 0 -- true (E-ISZEROZERO) iszero (succ nvı) - false (E-ISZEROSUCC) ti iszero ti ti iszerot (E-ISZERO) Figure 3-2: Arithmetic expressions (NB)
– (untyped) Syntax t Evaluation t-t' = Х terms: variable abstraction application ti — tí ti t2 — tít2 (E-APP1) ax.t tt t2 —- tz Vi t2 —— Vi t' (E-APP2) V values: abstraction value dx.t (Ax.t12) V2 -- [x - V2]t12 - (E-APPABS) Figure 5-3: Untyped lambda-calculus (4)