第15回：Specification and Verification of Software with CafeOBJ -Part 4 - Modules
「Answer to the challenge」
This blog continues Part 1 (リンク ») Part 2 (リンク ») and Part 3 (リンク ») of our series on software specification and verification with CafeOBJ.
In the last part we have made our first steps with CafeOBJ, learned how start and quit the interpreter, how to access the help system, and how to write basic functions. This time we will turn our attention to the most fundamental building blocks of specifications, modules.
「Answer to the challenge」
But before diving into modules, let us give answers to the challenge posed at the end of the last blog, namely to give definitions of the factorial function and the Fibonacci function. Without much discussion, here is the one possible solution for the Fibonacci numbers:
-- Factorial
open NAT .
op _! : Nat -> Nat .
eq 0 ! = 1 .
eq ( X:NzNat ! ) = X * ( (p X) ! ) .
red 10 ! .
close
-- Fibonacci
open NAT .
op fib : Nat -> Nat .
eq fib ( 0 ) = 0 .
eq fib ( 1 ) = 1 .
ceq fib ( X:Nat ) = fib (p X) + fib (p (p X)) if X > 1 .
red fib(10) .
close
Note that in the case of factorial we used the standard mathematical notation of postfix bang. We will come to the allowed syntax later on.
「Modules」
Modules are the basic building blocks of CafeOBJ specifications, and they correspond - or define - order-sorted algebras. Think about modules as a set of elements, operators on these elements, and rules how they behave. A very simple example of such a module is:
module ADDMOD {
[ Elem ]
op _+_ : Elem Elem -> Elem .
op 0 : -> Elem .
eq 0 + A:Elem = A .
}
This modules is introduced using the keyword module and the identifier ADDMOD, and the definition is enclosed in curly braces. The first line [ Elem ] defines the types (or sorts) available in the module. Most algebra one sees is mono-sorted, so there is only one possible sort, but algebras in CafeOBJ are many-sorted, and in fact order-sorted (we come to that later). So the module we are defining contains only elements of one sort Elem.
Next up are two lines starting with op, which introduces operators. Operators (think "functions") have a certain arity, that is, the take a certain number of arguments and return a value. In the many-sorted case we not only need to specify how many arguments an operator takes, but also from which sorts these arguments are. In the above case, let us first look at the line op _+_ : Elem Elem -> Elem .. Here an infix operator + is introduced, that takes two arguments of sort Elem, and returns again an Elem.
The next line defines an operator 0 - you might ask what a strange operator this is, but looking at the definition we see that there is no arguments to the operator, only a result. This is the standard way to define constants. So we now have an addition operator and a constant operator.
The last line of the definition starts with eq which introduces an equality, or axiom, or rule. It states that the left side and the right side are equal, in mathematical terms, that 0 is a left-neutral element of +.
Even with much more complicated modules, these three blocks will form most of the code one writes in CafeOBj: sort declarations, operator declarations, axiom definitions.
「A first module」
Let us define a bit more involved module extending the ideas of the pet example above:
mod! PNAT {
[ PNat ]
op 0 : -> PNat .
op s : PNat -> PNat .
op _+_ : PNat PNat -> PNat .
vars X Y : PNat
eq 0 + Y = Y .
eq s(X) + Y = s(X + Y) .
}
You will immediately recognize the same parts as in the first example, sort declaration, three operator declarations, and two axioms. There are two things that are new: (1) the module started with mod!: mod is a shorthand for the longer module, and the bang after it indicates that we are considering initial models - we wont go into details about initial versus free models here, though; (2) the line vars X Y : PNat: we have seen variable declarations inline in the first example A:Elem, but instead of this inline definition of variables one can defines variables beforehand and use them later on multiple times.
For those with mathematical background, you might have recognized that the name of the module (PNAT) relates to the fact that we are defining Peano Natural Numbers here. For those with even more mathematical background - yes I know this is not the full definition of Peano numbers ;-)
Next, let us see what we can do with this module, in particular what are elements of this algebra and how we can add them. From the definiton we only see that 0 is a constant of the algebra, and that the monadic operator s defines new elements. That means, that terms of the form 0, s(0), s(s(0)), s(s(s(0))) etc are PNats . So, can we do computations with these kind of numbers? Let us see:
CafeOBJ> open PNAT .
-- opening module PNAT.. done.
%PNAT> red s(s(s(0))) + s(s(0)) .
-- reduce in %PNAT : (s(s(s(0))) + s(s(0))):PNat
(s(s(s(s(s(0)))))):PNat
(0.0000 sec for parse, 0.0010 sec for 4 rewrites + 7 matches)
%PNAT> close
CafeOBJ>
Oh, CafeOBJ computed something for us. Let us look into details of the computation. CafeOBJ has a built-in tracing facility that shows each computations step. It is activated using the code set trace whole on:
%PNAT> set trace whole on
%PNAT> red s(s(s(0))) + s(s(0)) .
-- reduce in %PNAT : (s(s(s(0))) + s(s(0))):PNat
[1]: (s(s(s(0))) + s(s(0))):PNat
---> (s((s(s(0)) + s(s(0))))):PNat
[2]: (s((s(s(0)) + s(s(0))))):PNat
---> (s(s((s(0) + s(s(0)))))):PNat
[3]: (s(s((s(0) + s(s(0)))))):PNat
---> (s(s(s((0 + s(s(0))))))):PNat
[4]: (s(s(s((0 + s(s(0))))))):PNat
---> (s(s(s(s(s(0)))))):PNat
(s(s(s(s(s(0)))))):PNat
(0.0000 sec for parse, 0.0000 sec for 4 rewrites + 7 matches)
The above trace shows that the rule (axiom) eq s(X) + Y = s(X + Y) . is applied from left to right until the final term is obtained.
「Computational model of CafeOBJ」
The underlying computation mechanism of CafeOBJ is Term Rewriting, in particular order-sorted conditional term rewriting with associativity and commutativity (AC). Just as a side node, CafeOBJ is one of the very few (if not the only one still in use) system that implements conditional AC rewriting, in addition on order-sorted terms.
We wont go into details of the intricacies of term rewriting but mention only one thing that is important for the understanding of the computational model of the CafeOBJ interpreter: While axioms (equations) do not have a direction, they are just statements of equality between two terms, the evaluation carried out by the red uses the axioms only in the direction from left to right, thus it is important how an equation is written down. General rule is to write the complex term on the left side and the simple term on the right (if it is easy to define what is the more complex one).
Let us exhibit this directional usage on a simple example. Look at the following code, what will happen?
mod! FOO {
[ Elem ]
op f : Elem -> Elem .
op a : -> Elem .
var x : Elem
eq f(x) = f(f(x)) .
}
set trace whole on
open FOO .
red f(a) .
I hope you guessed it, we will send CafeOBJ into an infinite loop:
%FOO> red f(a) .
-- reduce in %FOO : (f(a)):Elem
[1]: (f(a)):Elem
---> (f(f(a))):Elem
[2]: (f(f(a))):Elem
---> (f(f(f(a)))):Elem
[3]: (f(f(f(a)))):Elem
---> (f(f(f(f(a))))):Elem
[4]: (f(f(f(f(a))))):Elem
...
This is because the rules are strictly applied from left to right, and this can be done again and again.
・・・ここから先は、アクセリア株式会社で公開中のコラム本編でご覧ください。
(リンク »)
【アクセリア株式会社の研究開発部社員：Norbert Preining氏のコラム】
・第1回：今さら聞けない、機械学習/ディープラーニングとは！？ (リンク »)
・第2回：最新の機械学習の代表、ニューラルネットワークとは (リンク »)
・第3回：手書き数字を認識する機械学習 (リンク »)
・第4回：畳み込みニューラルネットワーク (リンク »)
・第5回：機械学習における今後の展開 (リンク »)
・第9回：Analyzing Debian packages with Neo4j (リンク »)
・第10回：Analyzing Debian packages with Neo4j - Part 2 UDD and Graph DB Schema (リンク »)
・第11回：Analyzing Debian packages with Neo4j - Part 3 Getting data from UDD into Neo4j (リンク »)
・第12回：Specification and Verification of Software with CafeOBJ - Part 1 - Introducing CafeOBJ (リンク »)
・第13回：Specification and Verification of Software with CafeOBJ - Part 2 - Basics of CafeOBJ (リンク »)
・第14回：Specification and Verification of Software with CafeOBJ - Part 3 - First steps with CafeOBJ (リンク »)
【アクセリア株式会社の研究開発部社員のコラム】
・第6回：アクセリアが手がけるP2P (Peer-to-Peer) (リンク »)
・第7回：効率的な検索を可能にする、グラフデータベース (リンク »)
・第8回：アクセリアにおけるディープラーニング適用例 (リンク »)
This blog continues Part 1 (リンク ») Part 2 (リンク ») and Part 3 (リンク ») of our series on software specification and verification with CafeOBJ.
In the last part we have made our first steps with CafeOBJ, learned how start and quit the interpreter, how to access the help system, and how to write basic functions. This time we will turn our attention to the most fundamental building blocks of specifications, modules.
「Answer to the challenge」
But before diving into modules, let us give answers to the challenge posed at the end of the last blog, namely to give definitions of the factorial function and the Fibonacci function. Without much discussion, here is the one possible solution for the Fibonacci numbers:
-- Factorial
open NAT .
op _! : Nat -> Nat .
eq 0 ! = 1 .
eq ( X:NzNat ! ) = X * ( (p X) ! ) .
red 10 ! .
close
-- Fibonacci
open NAT .
op fib : Nat -> Nat .
eq fib ( 0 ) = 0 .
eq fib ( 1 ) = 1 .
ceq fib ( X:Nat ) = fib (p X) + fib (p (p X)) if X > 1 .
red fib(10) .
close
Note that in the case of factorial we used the standard mathematical notation of postfix bang. We will come to the allowed syntax later on.
「Modules」
Modules are the basic building blocks of CafeOBJ specifications, and they correspond - or define - order-sorted algebras. Think about modules as a set of elements, operators on these elements, and rules how they behave. A very simple example of such a module is:
module ADDMOD {
[ Elem ]
op _+_ : Elem Elem -> Elem .
op 0 : -> Elem .
eq 0 + A:Elem = A .
}
This modules is introduced using the keyword module and the identifier ADDMOD, and the definition is enclosed in curly braces. The first line [ Elem ] defines the types (or sorts) available in the module. Most algebra one sees is mono-sorted, so there is only one possible sort, but algebras in CafeOBJ are many-sorted, and in fact order-sorted (we come to that later). So the module we are defining contains only elements of one sort Elem.
Next up are two lines starting with op, which introduces operators. Operators (think "functions") have a certain arity, that is, the take a certain number of arguments and return a value. In the many-sorted case we not only need to specify how many arguments an operator takes, but also from which sorts these arguments are. In the above case, let us first look at the line op _+_ : Elem Elem -> Elem .. Here an infix operator + is introduced, that takes two arguments of sort Elem, and returns again an Elem.
The next line defines an operator 0 - you might ask what a strange operator this is, but looking at the definition we see that there is no arguments to the operator, only a result. This is the standard way to define constants. So we now have an addition operator and a constant operator.
The last line of the definition starts with eq which introduces an equality, or axiom, or rule. It states that the left side and the right side are equal, in mathematical terms, that 0 is a left-neutral element of +.
Even with much more complicated modules, these three blocks will form most of the code one writes in CafeOBj: sort declarations, operator declarations, axiom definitions.
「A first module」
Let us define a bit more involved module extending the ideas of the pet example above:
mod! PNAT {
[ PNat ]
op 0 : -> PNat .
op s : PNat -> PNat .
op _+_ : PNat PNat -> PNat .
vars X Y : PNat
eq 0 + Y = Y .
eq s(X) + Y = s(X + Y) .
}
You will immediately recognize the same parts as in the first example, sort declaration, three operator declarations, and two axioms. There are two things that are new: (1) the module started with mod!: mod is a shorthand for the longer module, and the bang after it indicates that we are considering initial models - we wont go into details about initial versus free models here, though; (2) the line vars X Y : PNat: we have seen variable declarations inline in the first example A:Elem, but instead of this inline definition of variables one can defines variables beforehand and use them later on multiple times.
For those with mathematical background, you might have recognized that the name of the module (PNAT) relates to the fact that we are defining Peano Natural Numbers here. For those with even more mathematical background - yes I know this is not the full definition of Peano numbers ;-)
Next, let us see what we can do with this module, in particular what are elements of this algebra and how we can add them. From the definiton we only see that 0 is a constant of the algebra, and that the monadic operator s defines new elements. That means, that terms of the form 0, s(0), s(s(0)), s(s(s(0))) etc are PNats . So, can we do computations with these kind of numbers? Let us see:
CafeOBJ> open PNAT .
-- opening module PNAT.. done.
%PNAT> red s(s(s(0))) + s(s(0)) .
-- reduce in %PNAT : (s(s(s(0))) + s(s(0))):PNat
(s(s(s(s(s(0)))))):PNat
(0.0000 sec for parse, 0.0010 sec for 4 rewrites + 7 matches)
%PNAT> close
CafeOBJ>
Oh, CafeOBJ computed something for us. Let us look into details of the computation. CafeOBJ has a built-in tracing facility that shows each computations step. It is activated using the code set trace whole on:
%PNAT> set trace whole on
%PNAT> red s(s(s(0))) + s(s(0)) .
-- reduce in %PNAT : (s(s(s(0))) + s(s(0))):PNat
[1]: (s(s(s(0))) + s(s(0))):PNat
---> (s((s(s(0)) + s(s(0))))):PNat
[2]: (s((s(s(0)) + s(s(0))))):PNat
---> (s(s((s(0) + s(s(0)))))):PNat
[3]: (s(s((s(0) + s(s(0)))))):PNat
---> (s(s(s((0 + s(s(0))))))):PNat
[4]: (s(s(s((0 + s(s(0))))))):PNat
---> (s(s(s(s(s(0)))))):PNat
(s(s(s(s(s(0)))))):PNat
(0.0000 sec for parse, 0.0000 sec for 4 rewrites + 7 matches)
The above trace shows that the rule (axiom) eq s(X) + Y = s(X + Y) . is applied from left to right until the final term is obtained.
「Computational model of CafeOBJ」
The underlying computation mechanism of CafeOBJ is Term Rewriting, in particular order-sorted conditional term rewriting with associativity and commutativity (AC). Just as a side node, CafeOBJ is one of the very few (if not the only one still in use) system that implements conditional AC rewriting, in addition on order-sorted terms.
We wont go into details of the intricacies of term rewriting but mention only one thing that is important for the understanding of the computational model of the CafeOBJ interpreter: While axioms (equations) do not have a direction, they are just statements of equality between two terms, the evaluation carried out by the red uses the axioms only in the direction from left to right, thus it is important how an equation is written down. General rule is to write the complex term on the left side and the simple term on the right (if it is easy to define what is the more complex one).
Let us exhibit this directional usage on a simple example. Look at the following code, what will happen?
mod! FOO {
[ Elem ]
op f : Elem -> Elem .
op a : -> Elem .
var x : Elem
eq f(x) = f(f(x)) .
}
set trace whole on
open FOO .
red f(a) .
I hope you guessed it, we will send CafeOBJ into an infinite loop:
%FOO> red f(a) .
-- reduce in %FOO : (f(a)):Elem
[1]: (f(a)):Elem
---> (f(f(a))):Elem
[2]: (f(f(a))):Elem
---> (f(f(f(a)))):Elem
[3]: (f(f(f(a)))):Elem
---> (f(f(f(f(a))))):Elem
[4]: (f(f(f(f(a))))):Elem
...
This is because the rules are strictly applied from left to right, and this can be done again and again.
・・・ここから先は、アクセリア株式会社で公開中のコラム本編でご覧ください。
(リンク »)
【アクセリア株式会社の研究開発部社員：Norbert Preining氏のコラム】
・第1回：今さら聞けない、機械学習/ディープラーニングとは！？ (リンク »)
・第2回：最新の機械学習の代表、ニューラルネットワークとは (リンク »)
・第3回：手書き数字を認識する機械学習 (リンク »)
・第4回：畳み込みニューラルネットワーク (リンク »)
・第5回：機械学習における今後の展開 (リンク »)
・第9回：Analyzing Debian packages with Neo4j (リンク »)
・第10回：Analyzing Debian packages with Neo4j - Part 2 UDD and Graph DB Schema (リンク »)
・第11回：Analyzing Debian packages with Neo4j - Part 3 Getting data from UDD into Neo4j (リンク »)
・第12回：Specification and Verification of Software with CafeOBJ - Part 1 - Introducing CafeOBJ (リンク »)
・第13回：Specification and Verification of Software with CafeOBJ - Part 2 - Basics of CafeOBJ (リンク »)
・第14回：Specification and Verification of Software with CafeOBJ - Part 3 - First steps with CafeOBJ (リンク »)
【アクセリア株式会社の研究開発部社員のコラム】
・第6回：アクセリアが手がけるP2P (Peer-to-Peer) (リンク »)
・第7回：効率的な検索を可能にする、グラフデータベース (リンク »)
・第8回：アクセリアにおけるディープラーニング適用例 (リンク »)
本プレスリリースは発表元企業よりご投稿いただいた情報を掲載しております。
お問い合わせにつきましては発表元企業までお願いいたします。
お問い合わせにつきましては発表元企業までお願いいたします。
