表現(xiàn)系工學(xué)特論課件

1、知能特論項(xiàng)書換系（）代數(shù)的仕様項(xiàng)書換 Term Rewriting Systems(1)Algebraic Specification and Term RewritingIntelligent Software第1頁(yè)，共27頁(yè)。項(xiàng)書換系入門：基本的等式等式書換規(guī)則書換仕様計(jì)算書換規(guī)則左辺対応右辺(equation)(rewrite rule)(rewriting)(specification)(program)(computation) (Introduction to term rewriting systems: Basic idea)(an instance of the left-h

2、and side of a rewrite rule)(the corresponding instance of the right-hand side)第2頁(yè)，共27頁(yè)。項(xiàng)書換系入門：応用記號(hào)計(jì)算定理証明代數(shù)的仕様記述自動(dòng)検証(symbolic computation)(theorem proving)(algebraic specification of software)(automated verification of software) (Introduction to term rewriting systems: Applications)第3頁(yè)，共27頁(yè)。項(xiàng)書換系構(gòu)文論 (

3、1/2) (Syntax of term rewriting systems)Atomic symbols used in term rewriting systems are classified into variables (x,y,z,), constants (0,1,a,b,c,), and function symbols (f,g,h,) with fixed arity, the number of arguments they take.A term is constructed as follows.A variable and a constant are terms.

4、If f is a function symbol of arity n and if t1 , tn are terms, then f(t1,tn) is a term.基本的記號(hào)次種類第4頁(yè)，共27頁(yè)。項(xiàng)書換系構(gòu)文論 (2/2) (Syntax of term rewriting systems)A rewrite rule is an ordered pair lr of terms (the left-hand side l and the right-hand side r).Any instance of l can be rewritten to the correspondi

5、ng instance of r.A term rewriting system (TRS) R is a set of rewrite rules.第5頁(yè)，共27頁(yè)。項(xiàng)書換系操作的意味論 (1/5)左辺(instance: 実例）部分項(xiàng)(reducible expression)A term s is reducible to a term t, notation sRt (or st), if t can be obtained by applying a rewrite rule in R once to a subterm (a part) of s.subterm (Operatio

6、nal semantics of term rewriting)an instance of the left-hand sidea redex(reducible expression)第6頁(yè)，共27頁(yè)。項(xiàng)書換系操作的意味論 (2/5)A rewrite sequence represents a computation. (Operational semantics of term rewriting)A term tn is a normal form of the initial term t0 if tn cannot be rewritten any more.The normal

7、 form represents the result of the computation.第7頁(yè)，共27頁(yè)。項(xiàng)書換系操作的意味論 (3/5) (Operational semantics of term rewriting)Rewrite strategy: In general, the computation is non-deterministic, i.e., there are many ts to which s is reducible. A rewrite strategy determines which one to choose.Leftmost-innermost

8、strategy chooses the leftmost redex from the innermost ones. Here is an example.第8頁(yè)，共27頁(yè)。項(xiàng)書換系操作的意味論 (4/5) (Operational semantics of term rewriting)Leftmost-outermost strategy chooses the leftmost redex from the outermost ones. 第9頁(yè)，共27頁(yè)。項(xiàng)書換系操作的意味論 (5/5)第回扱第回扱 (Operational semantics of term rewriting)

9、A TRS is terminating (or has a termination property) if there exists no infinite rewrite sequence., i.e., the computation will terminate definitely .A TRS is confluent (or has a confluence property) if there exists no or unique normal form, i.e., there exists at most one result of the computation.di

10、scuss it in the second lecture. discuss it in the third lecture. 第10頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (1/13) (Algebraic specification of software)Algebraic specifications define abstract data types by describing relationships among functions in a set of equations.Direct execution of algebraic specifications as TRSs ar

11、e possible by directing equations l=r to lr.第11頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (2/13)例題 (Example 1: Stack) (Algebraic specification of software)第12頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (3/13) (Algebraic specification of software)(Example of direct execution)第13頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (4/13) 0 s(x) 第引數(shù)來(lái)自然數(shù)場(chǎng)合盡 (Algebraic specification of software)(E

12、xample 2: Addition of natural numbers)The successor function s(x)=x+1 allows us to represent the natural numbers as terms 0, s(0), s(s(0),The patterns 0 and s(x) cover all the cases for possible natural numbers for the first argument.例題：自然數(shù)加算第14頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (5/13) (Algebraic specification of softw

13、are)(Example of direct execution)2+2 4第15頁(yè)，共27頁(yè)。cons(H,T)補(bǔ)足構(gòu)造 (1/3)cell尾部tail頭部headH:T，項(xiàng)表現(xiàn)簡(jiǎn)易記法：:列A, B, C, 表現(xiàn)構(gòu)造 (Supplementary note: List structure)List structure is a data structure used to represent a sequence A, B, C, of data.B,C,AIt is implemented as a cell consisting of two parts: the head for r

14、epresenting the first idem of the list and the tail for the subsequence starting from the second item.The cell consisting of the head H and the tail T is represented by the term cons(H,T) and abbreviated as H:T.構(gòu)造 A,B,C,第16頁(yè)，共27頁(yè)。補(bǔ)足構(gòu)造 (2/3)空empty listatomA: (B: (C: NULL)= A,B,C = A: B: C: NULL: 右結(jié)合演

15、算子 (Supplementary note: List structure)The : is a right-associative operator.簡(jiǎn)易記法abbreviation第17頁(yè)，共27頁(yè)。補(bǔ)足構(gòu)造 (3/3)要素A,B 要素(A:NULL):B:NULL (Supplementary note: List structure)top-level elements第18頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (6/13)素?cái)?shù)昇順並無(wú)限先頭 n 番目返 (Algebraic specification of software)n番目小素?cái)?shù)例題n 番目小素?cái)?shù)（先頭 0 番目）素?cái)?shù)集合2,3,

16、5,7,11,Example 3: The nth smallest prime number (where 0th is the first one)The set of prime number is 2,3,5,7,11,.The leftmost-outermost strategy will reduce prime(2) to 5.prime(n) returns the nth smallest prime number. nth(L, n) returns the nth element of the list L.primes( ) returns the infinite

17、list of the prime numbers arranged in the ascending order.最外最左戦略 prime(2)5第19頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (7/13) (Algebraic specification of software)nth(L, n)L n 番目要素nth(L, n) returns the nth element of the list L The first (0th) element of x:y is x.The (n+1)th element of x:y is the nth element of y.第20頁(yè)，共27頁(yè)。代數(shù)

18、的仕様記述 (8/13)primes( )= 2, 3, 5, 7, 11, 13, (Algebraic specification of software)素?cái)?shù)昇順並無(wú)限ints(s(s(0)= 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13,primes( ) returns the infinite list of the prime numbers in the ascending order.sieve ints(x) returns the infinite list of the natural numbers starting from the

19、natural number x in the ascending order.自然數(shù) x 以降自然數(shù)無(wú)限第21頁(yè)，共27頁(yè)。23456789101112131415162345678910111213141516代數(shù)的仕様記述 (9/13)2 : filter 3,4,5,6,7, by 2, followed by sieve2 : 3 : filter 5,7,9,11,13,15, by 3, followed by sievesieve 2,3,4,5,6,7,8,9,10,11,12,13,14,15,16, 2 : sieve 3,5,7,9,11,13,15, (Algebra

20、ic specification of software)sieve(x:y) returns the list of prime numbers starting from x by filtering out the non-prime numbers from y based on the Eratosthenes sieve algorithm.第22頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (10/13) (Algebraic specification of software)filt(x, L) x 倍數(shù) L 削除filt(x, L) returns the list obtained fr

21、om the list L by filtering out all the multiples of x.If the first element y is divided by x (i.e., y mod x equals 0), then ignore y and continue the filtering of z,else save y for the head and continue the filtering of z for the tail.if(C, x, y) represents the conditional expression. It returns x i

22、f the condition C is reduced to true; or y if C is reduced to false.eq(x, y) means x=y andmod(y, x) means the remainder of yx. (Define them in the Exercise.)第23頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (11/13)遅延評(píng)価最外最左戦略2 s(s(0) 略f filt 略1引數(shù)関數(shù)prime, ints, sieve引數(shù)囲括弧省略 (Algebraic specification of software)(delayed evaluation)(l

23、eftmost outermost reduction strategy)For the simplicity of the expressions:the integers such as 2 represents the terms such as s(s(0),f is the abbreviation for filt,the parentheses surrounding the argument of unary functions prime, ints, and sieve are omitted.第24頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (12/13) (Algebraic specification of software)第25頁(yè)，共27頁(yè)。代數(shù)的仕様記述 (13/13) (Algebraic specification of software)第26頁(yè)，共27頁(yè)。演習(xí)問(wèn)題Exercise 5When the natural numbers are e