Lambda Calculus - Motivation - University Of Illinois Urbana-Champaign
Lambda Calculus - Motivation Programming Languages and Compilers (CS 421) Sasa Misailovic 4110 SC, UIUC 21A Based in part on slides by Mattox Beckman, as updated by Vikram Adve, Gul Agha, and Elsa L Gunter 11/25/2018 1 Aim is to capture the essence of functions, function applications, and evaluation calculus is a theory of computation “The Lambda Calculus: Its Syntax and Semantics”. H. P. Barendregt. North Holland, 1984 11/25/2018 2 11/26/2018 4 Lambda Calculus - Motivation All deterministic sequential programs may be viewed as functions from input (initial state and input values) to output (resulting state and output values). -calculus is a mathematical formalism of functions and functional computations Two flavors: typed and untyped 11/25/2018 3 Untyped -Calculus Untyped -Calculus Grammar Only three kinds of expressions: Variables: x, y, z, w, Abstraction: x. e (Function expression, think fun x - e) Application: e1 e2 11/25/2018 5 Formal BNF Grammar: expression :: variable abstraction application ( expression ) abstraction :: variable . expression application :: expression expression 11/25/2018 6 1
Untyped -Calculus Terminology Example Occurrence: a location of a subterm in a term Variable binding: x. e is a binding of x in e Bound occurrence: all occurrences of x in x. e Free occurrence: one that is not bound ( x. y y. y ( x. x y) x) x 1 2 3 4 567 8 9 Scope of binding: in x. e, all occurrences in e not in a subterm of the form x. e’ (same x) Free variables: all variables having free occurrences in a term 7 Example Label occurrences and scope: 11/25/2018 Untyped -Calculus Label occurrences and scope: free How do you compute with the -calculus? Roughly speaking, by substitution: ( x. e1) e2 * e1 [e2 / x] free ( x. y y. y ( x. x y) x) x 1 2 3 4 567 8 9 11/25/2018 9 Transition Semantics for -Calculus E -- E’’ E E’ -- E’’ E’ * Modulo all kinds of subtleties to avoid free variable capture 11/25/2018 Application (version 1 - Lazy Evaluation) ( x . E) E’ -- E[E’/x] Application (version 2 - Eager Evaluation) E’ -- E’’ ( x . E) E’ -- ( x . E) E’’ ( x . E) V -- E[V/x] V – Value variable or abstraction 10 How Powerful is the Untyped -Calculus? The untyped -calculus is Turing Complete 8 Can express any deterministic sequential computation Problems: 11/25/2018 How to express basic data: bools, integers, etc? How to express recursion? Constants, if then else, etc, are conveniences; can be added as syntactic sugar (more on this later this week!) 12 2
Typed vs Untyped -Calculus The pure -calculus has no notion of type: (f f) is a legal expression! Types restrict which applications are valid Uses of -Calculus Simply typed -calculus is less powerful than the untyped -Calculus: NOT Turing Complete (no general recursion). See e.g.: Conversion (aka Substitution) 15 11/25/2018 16 Equivalence Let be a relation on lambda terms. Then is a congruence if: It is an equivalence relation equivalence is the smallest congruence containing conversion Reflexive, symmetric, transitive And if e1 e2 then (e e1) (e e2) and (e1 e) (e2 e) x. e1 x. e2 11/25/2018 14 1. Error: y is not free in the second term x. x y -- -- y. y y 2. Error: free occurrence of x becomes bound in wrong way when replaced by y x. y. x y -- -- y. y. y y exp exp[y/x] But x. ( y. y) x -- -- y. ( y. y) y And y. ( y. y) y -- -- x. ( y. y) x Congruence 11/25/2018 Conversion Non-Examples -conversion: x. exp -- -- y. (exp [y/x]) Provided that 1. y is not free in exp 2. No free occurrence of x in exp becomes bound in exp when replaced by y 11/25/2018 lambda-calculus predecessor 13 Types aren’t syntactic sugar! They disallow some terms Typed and untyped -calculus used for theoretical study of sequential programming languages Sequential programming languages are essentially the -calculus, extended with predefined constructs, constants, types, and syntactic sugar Ocaml is close to -Calculus: fun x - exp x. exp let x e1 in e2 ( x. e2) e1 One usually treats -equivalent terms as equal - i.e. use equivalence classes of terms 17 Notation: e1 e2 “Equivalent up to renaming” 18 3
Example Substitution Show: x. ( y. y x) x y. ( x. x y) y x. ( y. y x) x -- -- z. ( y. y z) z So, x. ( y. y x) x z. ( y. y z) z ( y. y z) -- -- ( x. x z) So, ( y. y z) ( x. x z) So, z. ( y. y z) z z. ( x. x z) z z. ( x. x z) z -- -- y. ( x. x y) y Therefore: x. ( y. y x) x y. ( x. x y) y So, z. ( x. x z) z y. ( x. x y) y 11/26/2018 19 Substitution: Detailed Rules x [N / x] N y [N / x] y if y x (e1 e2) [N / x] ((e1 [N / x] ) (e2 [N / x] )) ( x. e) [N / x] ( x. e) ( y. e) [N / x] y. (e [N / x] ) provided y x and y not free in N Rename y in redex if necessary 11/25/2018 11/25/2018 20 ( y. y z) [( x. x y) / z] ? Problems? z in redex in scope of y binding y free in the residue 21 Example ( y. y z) [( x. x y) / z] -- -- ( w.w z) [( x. x y) / z] w. w ( x. x y) 11/25/2018 22 reduction Only replace free occurrences ( y. y z ( z. z)) [( x. x) / z] y. y ( x. x) ( z. z) Not y. y ( x. x) ( z. ( x. x)) 11/25/2018 P called redex; N called residue Provided that no variable free in P becomes bound in P [N / x] Rename bound variables in P to avoid capturing free variables of N Example P [N / x] means replace every free occurrence of variable x in redex P by residue N Defined on -equivalence classes of terms P [N / x] means replace every free occurrence of x in P by N 23 Rule: ( x. P) N -- -- P [N /x] Essence of computation in the lambda calculus Usually defined on -equivalence classes of terms 11/25/2018 24 4
Equivalence Example ( z. ( x. x y) z) ( y. y z) -- -- ( x. x y) ( y. y z) -- -- ( y. y z) y -- -- y z ( x. x x) ( x. x x) -- -- ( x. x x) ( x. x x) -- -- ( x. x x) ( x. x x) -- -- . 11/25/2018 25 Not all terms reduce to normal forms Not all reduction strategies will produce a normal form if one exists We will explore two common reduction strategies next! 27 Eager evaluation 11/25/2018 Computations may be infinite 11/25/2018 26 Always reduce the left-most application in a top-most series of applications (i.e. do not perform reduction inside an abstraction) Stop when term is not an application, or left-most application is not an application of an abstraction to a term 11/25/2018 28 Example 1 (Eagerly) reduce left of top application to an abstraction Then (eagerly) reduce argument Then -reduce the application 11/25/2018 equivalent to a term that can be reduced Hard fact (Church-Rosser): if e1 and e2 are -equivalent and both are normal forms, then they are equivalent Lazy evaluation: Order of Evaluation equivalence is the smallest congruence containing equivalence and reduction A term is in normal form if no subterm is ( z. ( x. x)) (( y. y y) ( y. y y)) Lazy evaluation: 29 Reduce the left-most application: ( z. ( x. x)) (( y. y y) ( y. y y)) -- -- ( x. x) 11/25/2018 30 5
Example 2 Example 1 ( z. ( x. x))(( y. y y) ( y. y y)) Eager evaluation: Reduce the operator of the top-most application to an abstraction: Done. Reduce the argument: ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x )(( y. y y) ( z. z)) -- -- ( z. ( x. x))(( y. y y) ( y. y y)) -- -- ( z. ( x. x))(( y. y y) ( y. y y)) -- -- ( z. ( x. x))(( y. y y) ( y. y y)) 11/25/2018 31 Example 2 11/25/2018 32 Example 2 ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x )(( y. y y) ( z. z)) -- -- ( x. x x )(( y. y y) ( z. z)) -- -- (( y. y y ) ( z. z)) (( y. y y ) ( z. z)) 11/25/2018 33 Example 2 11/25/2018 Example 2 ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x )(( y. y y) ( z. z)) -- -- (( y. y y ) ( z. z)) (( y. y y ) ( z. z) 11/25/2018 34 ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x )(( y. y y) ( z. z)) -- -- (( y. y y ) ( z. z)) (( y. y y ) ( z. z)) 35 11/25/2018 36 6
Example 2 Example 2 ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x )(( y. y y) ( z. z)) -- -- ( x. x x )(( y. y y) ( z. z)) -- -- (( y. y y ) ( z. z)) (( y. y y ) ( z. z)) (( y. y y ) ( z. z)) (( y. y y ) ( z. z)) -- -- (( z. z ) ( z. z))(( y. y y ) ( z. z)) -- -- (( z. z ) ( z. z))(( y. y y ) ( z. z)) 11/25/2018 37 Example 2 11/25/2018 Example 2 ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x )(( y. y y) ( z. z)) -- -- ( x. x x )(( y. y y) ( z. z)) -- -- (( y. y y ) ( z. z)) (( y. y y ) ( z. z)) (( y. y y ) ( z. z)) (( y. y y ) ( z. z)) -- -- (( z. z ) ( z. z))(( y. y y ) ( z. z)) -- -- (( z. z ) ( z. z))(( y. y y ) ( z. z)) -- -- ( z. z ) (( y. y y ) ( z. z)) 11/25/2018 39 Example 2 11/25/2018 40 Example 2 ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x )(( y. y y) ( z. z)) -- -- (( y. y y ) ( z. z) ) (( y. y y ) ( z. z)) -- -- (( z. z ) ( z. z))(( y. y y ) ( z. z)) -- -- ( z. z ) (( y. y y ) ( z. z)) -- -- ( y. y y ) ( z. z) ( x. x x )(( y. y y) ( z. z)) -- -- (( y. y y ) ( z. z)) (( y. y y ) ( z. z)) -- -- (( z. z ) ( z. z))(( y. y y ) ( z. z)) -- -- ( z. z ) (( y. y y ) ( z. z)) -- -- ( y. y y ) ( z. z) 11/25/2018 38 41 11/25/2018 42 7
Example 2 Example 2 ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x )(( y. y y) ( z. z)) -- -- (( y. y y ) ( z. z) ) (( y. y y ) ( z. z)) -- -- (( z. z ) ( z. z))(( y. y y ) ( z. z)) -- -- ( z. z ) (( y. y y ) ( z. z)) -- -- ( y. y y ) ( z. z) -- -- ( z. z) ( z. z) ( x. x x)(( y. y y) ( z. z)) Lazy evaluation: ( x. x x )(( y. y y) ( z. z)) -- -- (( y. y y ) ( z. z) ) (( y. y y ) ( z. z)) -- -- (( z. z ) ( z. z))(( y. y y ) ( z. z)) -- -- ( z. z ) (( y. y y ) ( z. z)) -- -- ( y. y y ) ( z. z) -- -- ( z. z) ( z. z) -- -- ( z. z) 11/25/2018 43 Example 2 ( x. x x)(( y. y y) ( z. z)) Eager evaluation: ( x. x x) (( y. y y) ( z. z)) -- -- ( x. x x)(( y. y y) ( z. z)) Eager evaluation: ( x. x x) (( y. y y) ( z. z)) -- -- ( x. x x) (( z. z ) ( z. z)) -- -- 45 Example 2 11/26/2018 46 Example 2 ( x. x x)(( y. y y) ( z. z)) Eager evaluation: ( x. x x) (( y. y y) ( z. z)) -- -- ( x. x x) (( z. z ) ( z. z)) -- -- ( x. x x) ( z. z) -- -- ( x. x x)(( y. y y) ( z. z)) Eager evaluation: ( x. x x) (( y. y y) ( z. z)) -- -- ( x. x x) (( z. z ) ( z. z)) -- -- ( x. x x) ( z. z) -- -- ( z. z) ( z. z) -- -- 11/26/2018 44 Example 2 11/26/2018 11/25/2018 47 11/26/2018 48 8
Untyped -Calculus Example 2 ( x. x x)(( y. y y) ( z. z)) Eager evaluation: ( x. x x) (( y. y y) ( z. z)) -- -- ( x. x x) (( z. z ) ( z. z)) -- -- ( x. x x) ( z. z) -- -- ( z. z) ( z. z) -- -- z. z 11/26/2018 49 How to Represent (Free) Data Structures (First Pass - Enumeration Types) type Represent each term as an abstraction: Let Ci x1 xn. xi 51 Functions over Enumeration Types 52 type C1 Cn match e with C1 - x1 Cn - xn Write a “match” function match e with C1 - x1 Cn - xn Think: give me what to do in each case and give the selector (the constructor expression), and I’ll apply that case 11/25/2018 11/25/2018 Functions over Enumeration Types x1 xn e. e x1 xn bool True False True x1. x2. x1 x. y. x False x1. x2. x2 x. y. y Think: you give me what to return in each case (think match statement) and I’ll return the case for the i‘th constructor 11/26/2018 50 How to Represent Booleans C1 Cn Notation – will write: x1 xn. e for x1. x2. xn. e e1 e2 en for (( ((e1 e2 ) e3) en-1) en 11/26/2018 Suppose is a type with n constructors: C1, ,Cn (no arguments) Only three kinds of expressions: Variables: x, y, z, w, Abstraction: x. e Application: e1 e2 53 Recall: Ci x1 xn. xi Then: match x1 xn e. e x1 xn e expression (single constructor instance). Then, “match Ci” selects xi 54 9
match for Booleans match for Booleans bool True False True x1 x2. x1 x y. x False x1 x2. x2 x y. y bool True False True x1 x2. x1 x y. x False x1 x2. x2 x y. y matchbool ? 11/25/2018 55 How to Write Functions over Booleans 11/25/2018 matchbool x1 x2 b ( x1 x2 b . b x1 x2 ) x1 x2 b 57 Example: 11/26/2018 58 59 Suppose is a type with n constructors: type C1 t11 t1k Cn tn1 tnm, Represent each term as an abstraction: Ci ti1 tij, x1 xn. xi ti1 tij, Ci ti1 tij, x1 xn . xi ti1 tij, not b. b ( x y. y)( x y. x) Try other operators: and, or, xor 11/25/2018 b x1 x2 if then else b x1 x2. (matchbool x1 x2 b) b x1 x2. ( x1 x2 b . b x1 x2 ) x1 x2 b b x1 x2. b x1 x2 How to Represent (Free) Data Structures (Second Pass - Union Types) not b match b with True - False False - True (matchbool) False True b ( x1 x2 b . b x1 x2 ) ( x y. y) ( x y. x) b b ( x y. y) ( x y. x) 56 How to Write Functions over Booleans Alternately: if b then x1 else x2 match b with True - x1 False - x2 if b then x1 else x2 if then else b x1 x2 b x1 x2 if then else b x1 x2 . b x1 x2 11/26/2018 matchbool x1 x2 e. e x1 x2 x y b. b x y Think: you need to give each constructor its arguments first 11/25/2018 60 10
How to Represent Pairs Functions over Pairs Pair has one constructor (comma) that takes two arguments type ( , ) pair (,) (a , b) x . x a b matchpair f p. p f fst p match p with (x,y) - x fst p. matchpair ( x y. x) ( f p. p f) ( x y. x) p. p ( x y. x) 11/26/2018 61 How to Represent (Free) Data Structures (Second Pass - Union Types) Suppose is a type with n constructors: type C1 t11 t1k Cn tn1 tnm, Represent each term as an abstraction: 11/25/2018 Ci ti1 tij, x1 xn. xi ti1 tij, Ci ti1 tij, x1 xn . xi ti1 tij, Think: you need to give each constructor its arguments first 11/26/2018 63 Write a “match” function match e with C1 y1 ym1 - f1 y1 ym1 Cn y1 ymn - fn y1 ymn match f1 fn e. e f1 fn Think: give me a function for each case and give me a case, and I’ll apply that case to the appropriate function with the data in that case 11/25/2018 Suppose is a type with n constructors: Suppose tih : (i.e. is recursive) type nat Suc nat 0 0 f x. x Suc n f x. f (n f x) Suc n f x. f (n f x) Such representation is called Church Numerals C1 t11 t1k Cn tn1 tnm, In place of a value tih have a function to compute the recursive value rih x1 xn Ci ti1 rih tij x1 xn . xi ti1 (rih x1 xn) tij Ci ti1 rih tij x1 xn . xi ti1 (rih x1 xn) tij 11/25/2018 64 How to Represent Natural Numbers How to Represent (Free) Data Structures (Third Pass - Recursive Types) 62 Functions over Union Types snd p. p ( x y. y) 65 11/26/2018 66 11
Some Church Numerals Some Church Numerals 2 Suc(Suc 0) ( n f x. f (n f x)) (Suc 0) -- ( n f x. f (n f x)) ( f x. f x) -- f x. f (( f x. f x) f x)) -- f x. f (( x. f x) x)) -- f x. f (f x) Apply a function twice “Do something (anything) once” 1 Suc 0 ( n f x. f (n f x)) ( f x. x) -- f x. f (( f x. x) f x) -- f x. f (( x. x) x) -- f x. f x Apply a function to its argument once “Do something (anything) once” 11/25/2018 67 Some Church Numerals 0 f x. x 1 f x. f x 2 f x. f f x 3 f x. f f f x 4 f x. f f f f x 5 f x. f f f f f x . n f x. f n x 11/26/2018 69 Write a “fold” function fold f1 fn match e with C1 y1 ym1 - f1 y1 ym1 Ci y1 rij yin - fn y1 (fold f1 fn rij) ymn Cn y1 ymn - fn y1 ymn fold f1 fn e. e f1 fn Match in non recursive case a degenerate version of fold 11/25/2018 fold f z n. n f z is zero n fold ( r. False) True n ( f x. f n x) ( r. False) True (( r. False) n ) True if n 0 then True else False 11/25/2018 70 Adding Church Numerals fold f z n match n with 0 - z Suc m - f (fold f z m) 68 Primitive Recursive Functions Primitive Recursion over Nat In general n f x. f ( (f x) ) with n applications of f (do “something” n times) 71 n f x. f n x and m f x. f m x n m f x. f (n m) x f x. f n (f m x) f x. n f (m f x) n m f x. n f (m f x) Subtraction is harder (needs to refer to predecessors) 11/25/2018 72 12
Multiplying Church Numerals How much is 2 2 ? ̅ n m f x. n f ( m x) ̅2̅ f x. f (f x) ̅2̅ f x. f (f x) So let’s begin: ( n m f x . n f (m f x) ) ̅2̅ ̅2̅ -- -- f x. ( f x. f (f x)) f ( ( f x. f (f x)) f x) -- -- f x. ( f x. f (f x)) f (f (f x)) -- -- f x. f (f (f (f x)) ̅4̅ 73 Predecessor and m f x. f m x n m f x. (f n m) x f x. (f m)n x f x. n (m f) x n m f x. n (m f) x How much is ̅2̅ ̅*̅ ̅2̅ ? 11/26/2018 74 Recursion: Y-Combinator (the original one) let pred aux n match n with 0 - (0,0) Suc m - (Suc(fst(pred aux m)), fst(pred aux m) fold ( r. (Suc(fst r), fst r)) (0,0) n n f x. f n x pred n. snd (pred aux n) n n. snd (fold ( r.(Suc(fst r), fst r)) (0,0) n) Want a -term Y such that for all terms R we have Y R R (Y R) Y needs to have replication to “remember” a copy of R Y y. ( x. y (x x)) ( x. y (x x)) Y R ( x. R(x x)) ( x. R(x x)) R (( x. R(x x)) ( x. R(x x))) Notice: Requires lazy evaluation (see example 1 on eager vs lazy much earlier in this deck!) 11/25/2018 75 # let rec y f f (y f);; val y : ('a - 'a) - 'a fun Let F f n. if n 0 then 1 else n * f (n - 1) # let mk fact fun f n - if n 0 then 1 else n * f(n-1);; val mk fact : (int - int) - int - int fun Y F 3 F (Y F) 3 if 3 0 then 1 else 3 * ((Y F)(3 - 1)) 3 * (Y F) 2 3 * (F(Y F) 2) 3 * (if 2 0 then 1 else 2 * (Y F)(2 - 1)) 3 * (2 * (Y F)(1)) 3 * (2 * (F(Y F) 1)) 3 * 2 * 1 * (if 0 0 then 1 else 0*(Y F)(0 -1)) 3*2*1*1 6 11/25/2018 76 Y in OCaml Factorialb 11/25/2018 # y mk fact;; Stack overflow during evaluation (looping recursion?). 77 11/25/2018 78 13
Eager Evaluation of Y in Ocaml Some Other Combinators # let rec y f x f (y f) x;; val y : (('a - 'b) - 'a - 'b) - 'a - 'b fun More about Y-combinator: # y mk fact;; - : int - int fun For your general exposure: I x.x K x. y. x K* x. y. y S x. y. z. x z (y z) https://en.wikipedia.org/wiki/SKI combinator calculus # y mk fact 5;; - : int 120 Use recursion to get recursion 11/26/2018 79 https://mvanier.livejournal.com/2897.html 11/26/2018 80 14
Lambda Calculus - Motivation Aim is to capture the essence of functions, function applications, and evaluation calculus is a theory of computation "The Lambda Calculus: Its Syntax and Semantics". H. P. Barendregt. North Holland, 1984 11/25/2018 3 Lambda Calculus - Motivation All deterministic sequential programs may
1. Lambda service polls the shard once per second for a set of records. Then synchronously invokes the Lambda function with the batch of records. 2. If the Lambda returns successfully, the Lambda service advances to the next set of records and repeats step 1. 3. If the Lambda errors, by default the Lambda service invokes the
Sororites: Alpha Sigma Rho, Delta Phi Lambda, Delta Phi Omega, Lambda Theta Alpha, Sigma Sigma Rho, Theta Nu Xi Fraternities: Delta Epsilon Psi, Lambda Phi Epsilon, Lambda Upsilon Lambda, Lambda Theta Phi, Sigma Beta Rho, Xi Kappa. GREEK ALPHABET & TERMINOLOGY ACTIVE: a fully initiated member of the fraternity
Sororites: Alpha Sigma Rho, Delta Phi Lambda, Delta Phi Omega, Lambda Theta Alpha, Sigma Sigma Rho, Theta Nu Xi Fraternities: Delta Epsilon Psi, Lambda Phi Epsilon, Lambda Upsilon Lambda, Lambda Theta Phi, Sigma Beta Rho, Xi Kappa. GREEK ALPHABET & TERMINOLOGY ACTIVE: a fully initiated member of the fraternity
Lambda Calculus #2 Plan Introduce lambda calculus - Syntax - Substitution - Operational Semantics ( with contexts!) - Evaluation strategies - Equality Relationship to programming languages (next time) Study of types and type systems (later) #3 Lambda Background Developed in 1930's by Alonzo Church
AWS Lambda in (a bit of) theory and in action Adam Smolnik . A bit of a function theory The term Lambda (λ) originated from Lambda calculus - a theoretical universal model for describing functions . AWS Lambda service Enables implementations that are able to react quickly to events
AWS SAM-Lambda-Beispielvorlage . 183 Anwendungsfälle . 184 Beispiel 1: Amazon S3 pusht Ereignisse und ruft eine Lambda-Funktion auf . 185 Beispiel 2: AWS Lambda ruft Ereignisse aus einem Kinesis-Stream ab und ruft eine Lambda- .
The lambda calculus extends the idea of an expression language to include func-tions. Where we normallywrite Let f be the functionx x2. Then consider A f(5), in the lambda calculus we just write A (λx.x2)(5). The expressionλx.x2 stands forthe functionthat maps x to x2 (as opposedto the
Korean language textbooks and language teaching in terms of Korean honorifics. They have pointed out several problems in current teaching materials and emphasized the importance of pragmatic factors and the necessity of authentic data to fully reflect actual Korean honorific uses. Addressing these issues, the thesis demonstrates the need for teaching materials that introduce how honorific .
