Rubén Rubio

Narciso Martí-Oliet
email: narciso@ucm.es

Isabel Pita

Alberto Verdejo
email: jalberto@ucm.es

Parameterized Strategies Specification in Maude

Keywords: Rewriting logic, Strategies, Maude, Parameterized specification

Strategies and parameterization are two convenient tools for building clear and easily configurable specifications of complex computational systems, compositionally. Parameterization is a widely used feature of the Maude rewriting framework, whose strategy language implementation we have recently completed with strategy modules. This paper describes the Maude strategy language and the associated parameterization techniques. Then, the specification and analysis of some examples of strategy parameterized systems are shown.

Introduction

Strategies are ubiquitous in Computer Science. As recipes to tackle search problems and bound nondeterminism, they appear in algorithms, automatic deduction, language semantics, artificial intelligence, . . . . In rewriting logic [START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF], some of these examples are better specified compositionally, abstracting not only data representation and rules but also the way they are applied. This parametric control of the rewriting process is conveniently expressed using strategies that take other strategies as parameters.

Maude [START_REF] Clavel | All About Maude-A High-Performance Logical Framework[END_REF]7] is a declarative high-level language based on rewriting logic that allows the description, execution and analysis of concurrent and distributed system models at different levels. First, sorts, symbols, equations and membership axioms are expressed in terms of membership equational logic [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF]. Then, we add rewrite rules to represent transitions of a concurrent system, which need neither be deterministic, nor confluent, nor terminating. Above this, we can control how rules are applied using a strategy language [START_REF] Eker | Deduction, strategies, and rewriting[END_REF][START_REF] Martí-Oliet | Towards a strategy language for Maude[END_REF]. Its implementation, at the Core Maude level in C++, has been recently completed as an extension of Maude 2.7.1 [7].

The strategy language is based in its authors experience with strategies in Maude and in previous strategy languages like ELAN [START_REF] Borovanský | Rewriting with strategies in ELAN: A functional semantics[END_REF] and Stratego [START_REF] Bravenboer | Stratego/XT 0.17. A language and toolset for program transformation[END_REF]. It has already been exploited in the specification of algorithms, inference systems, and language semantics: Milner's CCS [START_REF] Martí-Oliet | Strategies and simulations in a semantic framework[END_REF], the ambient calculus [START_REF] Martí-Oliet | Strategies and simulations in a semantic framework[END_REF], the semantics of the parallel functional language Eden [START_REF] Hidalgo-Herrero | Using Maude and its strategies for defining a framework for analyzing Eden semantics[END_REF], equational logic completion procedures [START_REF] Verdejo | Basic completion strategies as another application of the Maude strategy language[END_REF], a proof calculus for membrane systems [START_REF] Andrei | Strategy-based proof calculus for membrane systems[END_REF], etc. These examples are likely to be expressed and generalized using control parameterization with strategies, whose implementation was not available at that time. Once expressed in this way, the specified systems can be both executed and tested with different alternative strategies provided as parameters, or analyzed at different levels with specific tools, like a model checker.

The next section introduces Maude, its strategy language, and the rudiments of parameterization. A generic backtracking scheme serves as an introductory example. The following sections describe some other examples of parameterized systems, targeting the simplex algorithm, the λ-calculus, and a functional program interpreter. These and more examples can be downloaded from [START_REF] Rubio | Strategy language for Maude web page[END_REF], as well as the current version of Maude with full strategy support.

Maude

A Maude program consists of a hierarchy of modules, describing the data representation and behavior of the system specified. There are different module types for different specification levels.

Functional modules define membership equational logic theories, whose signature (K, Σ, S) consists of a set of kinds K, a many-kinded collection of operators Σ = {Σ k1•••kn,k : (k 1 • • • k n , k) ∈ K * × K}, and S = {S k : k ∈ K} a many-kinded set of partially ordered sorts. Equations and sort membership axioms E are defined on them

(∀X) t = t t : s if i u i = u i ∧ j v j : s j
In addition, operators can be annotated with structural axioms, like commutativity (comm), associativity (assoc), and identity (id). For example, the following functional module specifies sets of integer numbers using both equations and axioms. System modules describe rewriting logic theories R = (Σ, E ∪ A, R), adding rewriting rules R on top of the equational theory. Rules do not have to be either confluent or terminating, so they are likely to express non-deterministic behavior. The module SUM-SET above introduces a rule sum that takes two integers in the set and replaces them by their sum.

(∀X) t ⇒ t if i u i = u i ∧ j v j : s j ∧ k w k ⇒ w k Anyhow,
Strategy modules allow finer control of the rule rewriting process by means of the strategy language and recursive strategy definitions. They are described in the next section.

The strategy language

Rules in rewriting logic can be applied in any order, at any position, and with different matches. Maude provides various commands, like rewrite and frewrite, that execute all available rules against a given term until none can be applied or an optional step bound is reached. They use some internal fixed criteria to select the next rule application. In turn, the search command explores all possible rewriting paths to find a target term meeting some conditions. However, the specifier is sometimes interested in imposing constrains on the allowed execution paths, like a particular precedence of rules, or to which subterms they must be applied, etc. This is when strategies get inside the game.

From the point of view of the results, a strategy α is an operation transforming a term t into a set of terms, since the restrictions need not make the process deterministic. Strategies can be executed with the command srewrite t using α. The most elementary strategy is rule application

top(label[x 1 <-t 1 , . . . , x n <-t n ]{α 1 , . . . ,α m }),
that executes any available rules with label label on any subterm of the subject term. Variables in the rule and its condition can be instantiated before application with the substitution that maps x k to t k , and if the rule contains any rewriting condition, it must be controlled with a substrategy α k . Moreover, the optional top modifier restricts the application of the rule to the top of the subject term. A more powerful tool for selecting where to apply a strategy is the matchrew operator matchrew P (x 1 , . . . , x n ) s.t. C by x 1 using α 1 , . . . , x n using α n It matches the pattern P on top of the subject term, and for each match satisfying the condition C, the subterms corresponding to x 1 , . . . , x n are rewritten using α 1 , . . . , α n , and reassembled again. The operator name can be prefixed by a or x to match anywhere within the term or modulo structural axioms. Similar format follow the tests match P s.t. C, to check if P matches the subject term and satisfies C. Regular expressions are included in the strategy language by means of the alternation α|β, the concatenation α;β, the Kleene star α * , and the constants idle and fail. A conditional strategy α ? β : γ is also available. It executes α and then β on its results, but if α does not produce any, it applies γ to the initial term.

The last ingredient of the strategy language are potentially recursive named strategies. These strategies are defined in strategy modules, which have the form smod M is ... endsm and contain:

-Strategy declarations strat sname : T1 ... Tn @ T, which state their parameter types T 1 to T n , and the type T of the subject terms the strategy will be applied to. -Strategy definitions sd sname(t 1 , . . . , t n ) := α. The free variables in the right-hand side strategy expression α must be included in the terms t 1 to t n . Conditional strategy definitions, introduced by csd, are available too, and impose conditions as in regular equations. A named strategy can be given any number of strategy definitions, and all definitions whose left-hand side matches the call term will be executed. Now, we will illustrate all the different strategy constructors described above with a very simple example. Consider the following system module:

mod SIMPLE i s s o r t Term . ops a b c d : → Term [ ctor ] . op f : Term → Term [ ctor ] . op g : Term Term → Term [ ctor ] . v a r s X Y : Term . r l [ ab ] : a ⇒ b . r l [ ac ] : a ⇒ c . r l [ bc ] : b ⇒ c . r l [ pf ] : f ( X ) ⇒ X . r l [ ad ] : f ( a ) ⇒ d . endm
The SIMPLE module defines some constants and functions to build terms, and various rules that transform them. For example, we can apply the pf rule to the term f(g(f(a), b)) by means of the srewrite command, whose initial keyword can be abbreviated to srew: Notice that all possible rewrites are returned as different solutions. In the first case, the rule can be applied both to the first and to the second occurrence of f. However, in the second case, the initial substitution restricts its application to the subterm f(a). Using the strategy top(pf) instead, pf is only applied on top and only g(f(a), b) is obtained. Finer precision on where to apply a strategy can be achieved by the subterm rewriting operator. For example, matchrew g(X, Y) by X using pf restricts the application to the first argument of g. Then g(f(b), f(c)) rewrites only to g(b, f(c)). Moreover, multiple subterms can be rewritten in parallel by strategies like amatchrew g(X, Y) by X using pf, Y using bc, which transforms the initial term f(g(f(a), b)) in f(g(a, c)).

Once we are able to apply strategies to particular subterms, we need regular expressions to compose rewriting sequences. If we rewrite g(a, b) by the concatenation ab ; bc, we obtain g(c, b) and g(b, c), since the rule bc has been applied after ab, at the same or at a different position. Instead, when executing the alternation ab | bc, only one of these is applied, and we get g(b, b) and g(a, c) as solutions. Finally, the iteration pf* applies pf zero or more times consecutively, so it rewrites f(f(a)) to f(f(a)), f(a), and a.

Other useful resources are the tests like match g(X, Y) s.t. X = Y. It does not produce any solution for g(a, a), but for g(a, b), the solution is the term itself. Tests easily combine with conditionals. For example, the strategy match f(X) ? ab : bc applies ab if the subject term top symbol is an f, and otherwise executes bc. Then, f(a) rewrites to f(b), b to c, and no solution is produced for a. However, conditionals can be used with any strategy as condition, as we will see soon and throughout the paper.

Finally, to define named and recursive strategies, we need to write strategy modules like the following: smod SIMPLE-STRAT i s p r o t e c t i n g SIMPLE . *** controls SIMPLE s t r a t rewrite @ Term . sd rewrite := all ? rewrite : idle . endsm where all is a built-in constant that executes any available rule. In this case, it can be seen as equivalent to ab | ac | bc | pf | ad. Hence, the strategy rewrite applies any rule until no more rules can be applied, as the usual rewrite command does. Running this strategy for the term g(f(a), f(b)) we obtain: In Figure 1, the strategy language semantics is described in brief. Apart from the initial term, the semantic function α : (X → T Σ/E ) × T Σ/E → P(T Σ/E ) receives a substitution by way of variable environment, because function calls and matchrews bind variables. The semantics of the strategy definitions δ is calculated as a fixed point of a continuous operator, and here ∆(sl, t 1 • • • t n ) refers to the set of strategy definitions for sl whose left-hand side matches t 1 , . . . , t n , along with the corresponding substitution σ.

Maude > srew g ( f ( a ) , f ( b )) using rewrite .

Parameterization

Parameterization is achieved using three basic building blocks: theories, views, and parameterized modules [START_REF] Clavel | All About Maude-A High-Performance Logical Framework[END_REF]7]. A parameterized module is a usual module taking a set of formal parameters, bound to some theories. mod NAME{X1 :: TH1, ..., XN :: THN} is ... endm.

A theory declares the interface, the syntactic and semantic requirements, the actual parameter must respect. Each module type (functional, system, strategy) has its theory counterpart. They are structurally identical, but theories are not required to fulfill the executability properties of a module. Module parameters can only be bound to theories of their type or simpler types. Finally, a view is the way to express how a module honors a theory, mapping each sort, operator, and strategy declared in the theory to the actual value in the module. Then, views are used to instantiate parameterized modules.

As an example, the most basic predefined theory is TRIV, which declares a single sort. δ (σ, t) Inside parameterized modules, sorts coming from theories are accessed by prefixing their names by their parameter name followed by a $ sign. Operators and strategies retain their names as in the parameter theory. The Maude standard prelude includes some general theories like TRIV, TOTAL-PREORDER, STRICT-WEAK-ORDER, . . . , and many views from the standard data types to those theories [START_REF] Clavel | All About Maude-A High-Performance Logical Framework[END_REF]7].

idle (θ, t) = {t} fail (θ, t) = ∅ α ; β (θ, t) = t ∈ α (θ,t) β (θ, t ) α | β (θ, t) = α (θ, t) ∪ β (θ, t) α* (θ, t) = n≥0 α n (θ, t) α ? β : γ (t) = α;β (θ, t) if α (θ, t) = ∅ γ (θ, t) if α (θ, t) = ∅ match P s.t. C (θ, t) = {t} if

An introductory example

A simple example of parameterized control is the generic backtracking scheme.

The abstract backtracking problem is specified in two nested theories, the first proclaims the functional requirements, and the second extends it with the strategic ones. They require a State sort for states, and a strategy expand to rewrite a state to any of its direct successors, non-deterministically. We admit that the generated successors may not be valid, so we require a predicate isOk to test them, and also a predicate isSolution to determine whether a given state is already a solution. Then, a parameterized module BT-STRAT, given the specification of the problem following BT-ELEMS, defines a strategy solve for executing the backtracking algorithm. This is the following module, where parameters are highlighted in italics.

f t h BT-ELEMS-BASE i s p r
smod BT-STRAT { X :: BT-ELEMS } i s s t r a t solve @ X$State . v a r S : X$State . sd solve := ( match S s . t . isSolution( S )) ? idle : (expand ; match S s . t . isOk( S ) ; solve ) . endsm

The solve strategy is recursive. It concludes successfully when it finds a solution. Otherwise, it applies the strategy expand to obtain a successor, tests whether it is valid, and iterates the process by a recursive call. Rewriting paths are discarded either when a successor not satisfying isOk is reached or when the expand strategy does not provide any successor. Indeed, each result of the expand strategy opens a new branch of the execution tree.

Although we call it backtracking, the strategy is abstract enough to be interpreted or executed otherwise, depending on the order in which the branches are explored. For backtracking, we understand a depth-first exploration, going backwards to try another branch when the current one has been exhausted without finding a solution. However, the default strategy rewriting implementation obeys a fair scheduling, which combines depth and breadth-first search. Here, the fair execution policy will usually require more time and memory usage than a real backtracking.

The generic algorithm is useless without actual instances. They can be specified in separate modules or files, but finally they have to fit in the frame of an abstract backtracking problem by means of a view from BT-ELEMS. eq isSolution ( graph (N , As , V P V )) = N == size ( V P ) . eq isSolution ( G : Graph ) = false [ owise ] . eq isOk ( graph (N , As , V P V )) = noCross ( V P ) . eq isOk ( graph (N , As , P )) = noCross ( P ) [ owise ] . r l [ next ] : graph (N , e (V , K ) As , P V ) ⇒ graph (N , As , P V K ) . endm

The module defines Graph, including both the graph and the current path, which can be extended up to a Hamiltonian cycle using the rule next whenever possible. Finally, as we said, the problem has to be presented as a backtracking instance using a view. Identity mappings do not need to be written, but we have included them to illustrate the syntax. This instance is specially simple, the expand strategy has been defined inline as the next rule. In general, more elaborated strategies can be defined in a strategy module. In that case, the strategy module must be the to part of the view and the strategy is mapped by strat expand to sname. This can be seen in other examples available in the webpage [START_REF] Rubio | Strategy language for Maude web page[END_REF] like the labyrinth escape problem, the n-queens problem, the graph m-coloring problem, etc.

v i
A refinement of backtracking is branch and bound. This algorithmic technique was also programmed with parameterized strategies. Its problem specification, its theories, include richer functional and strategic requirements, so we do not describe them here. In this case, we cannot use an expand strategy that nondeterministically evolves to a successor, we need to examine them all to decide which to explore first according to the rank function. Hence, we have experimented with multiple approaches using different problem signatures. These can also be downloaded from [START_REF] Rubio | Strategy language for Maude web page[END_REF].

The simplex algorithm

The simplex method [START_REF] Murty | Linear programming[END_REF] is a well-known algorithm for solving linear programming problems, i.e. for finding solutions that maximize (or minimize) a linear functional subject to some linear constraints.

max / min c 1 x 1 + • • • + c n x n a 11 x 1 + • • • + a 1n x n ≤ b 1 a 21 x 1 + • • • + a 2n x n = b 2 a 31 x 1 + • • • + a 3n x n ≥ b 3 x 1 , . . . , x n ≥ 0
Formulated by George Dantzig in the late 1940s, it has had many industrial applications. Here we present an executable linear programming solver written in Maude using this method. The various non-deterministic steps are controlled by strategies, which are configurable through parameterization.

Figure 2 shows all the specification modules. LINPROG includes some basic definitions of linear algebra (polynomials, inequalities, . . . , and operations on them), as well as linear programming problems. Then, SIMPLEX-TABLE defines the simplex tables (the state of the algorithm) and some operations to obtain information and modify them. At the rule level, SIMPLEX-CONSTR defines how to build a table from a linear programming problem, and SIMPLEX-EXECUTION provides the rules for the different actions of the simplex method. The most important is pivot, which changes the algorithm basis

c r l [ pivot ] : Table ⇒ pivot ( Table , Ve , Vl ) i f Ve , R := enterVars ( Table ) ∧ Vl , S := leaveVars ( Table , Ve ) .
This rule is non-deterministic because Ve and Vl can be chosen among different alternatives. Pivoting carelessly may even lead to cycles, so that the algorithm may not terminate. Fortunately, there are different cycle prevention techniques to avoid non-termination. The more common ones are the Bland rule and the lexicographic rule. These rules (or any other) can be switched by means of parameterization.

The global solving process starts with a linear programming problem. The first stage is the generation of the simplex table, a non-deterministic process which produces equivalent tables up to renaming. So, we will concentrate on the second stage, the simplex method itself.

sd solve := makeTable ; simplex . sd simplex := step ? simplex : idle . The simplex strategy executes a simplex step until no more can be applied. Each step first applies some rules that transform the table in some specific situations: unbounded detects when the problem is unbounded and transforms the table in a description of the beam of infinite improvement, and finish detects when the problem is already solved and presents the solution in a more readable form.

The other rules are related to the two phases method, which may be sometimes needed to find an initial feasible solution of the linear system: unfeas signals that the problem is unfeasible; and phase2 transforms the table to a usual table whenever possible. Finally, if none of these (cheaper and concluding) rules can be applied, the pivoting strategy pivotingStrat is applied. This is the parameter of the SIMPLEX-STRAT module, provided by the theory PIVOTING-STRAT, which declares a single strategy without parameters applicable to the simplex table sort. For instance, the Bland rule is specified in SIMPLEX-PIVOTING with the following strategy

sd bland := matchrew T s . t . Ve := minVar ( enterVars ( T )) ∧ Vl := minVar ( leaveVars (T , Ve )) by T u s i n g pivot [ Ve <-Ve , Vl <-Vl ] .
where minVar equationally computes the minimum variable within a set (a total order < is defined on them). A view Bland from PIVOTING-STRAT to SIMPLEX-PIVOTING, mapping pivotingStrat to bland, is then used to instantiate SIMPLEX-STRAT.

Parameterized analysis

A natural analysis of parameterized systems is the comparison of the behavior of their multiple instances, which can be executed or simulated, looking at the execution time, the number of rewriting steps, or the memory requirements. More essential properties can be inspected by tracing the state of the system while running the simulation. Strategies are a useful tool for that purpose. Apart from this, parameterized modules can be analyzed with specific tools like the Maude model checker.

For the simplex method, we have compared the performance of two pivoting strategies and free rewriting in terms of time and number of rewrites, against a linear programming exercises set. Since these properties depend on the actual Maude implementation, we also consider an intrinsic property of the algorithm: the number of iterations or pivoting steps until a solution is found. To obtain this attribute, we count the number of pivot rule executions with the aid of a parameterized analyzer module that maintains a pair watch(T, N) of a simplex table and a counter, applies the rules to the table using matchrew, and updates the counter accordingly. This can be compared with the unrestricted better case and worst case number of iterations, which can be calculated using strategies too. We observe that the lexicographic rule reduces the mean number of iterations, but since its decisions require more computations, its performance is similar to Bland's. The free strategy, executing the rules at the discretion of the Maude rewriting engine, performs quite well.

Free Bland Lexicographic

Regarding auxiliary tools, we have applied an experimental prototype of a strategy-aware model checker. Thanks to it, we can check whether the algorithm following a given strategy, for a fixed example, may cycle or not. Predictably, no example cycles with the Bland and lexicographic rules, but some do with free rewriting.

The λ-calculus

The λ-calculus can be easily expressed and executed in Maude [START_REF] Martí-Oliet | Rewriting Logic as a Logical and Semantic Framework[END_REF]. β-reduction is the single rule of the rewriting system, so a term can be reduced by simply using the rewrite and search commands.

s u b s o r t Var < LambdaTerm . op \ _._ : Var LambdaTerm → LambdaTerm [ ctor ] . op __ : LambdaTerm LambdaTerm → LambdaTerm [ ctor ] . r l [ beta ] : (\ x . M ) N ⇒ subst (M , x , N ) .
However, which β-redex is reduced first is an important choice. Some reduction paths may not terminate while others reach an irreducible term, even though this is unique by the Church-Rosser property. The normalization theorem says that reducing the leftmost outermost redex first guarantees finding a normal form in case it exists. We allow selecting which strategy step to use for a single reduction step and, using a parameterized module, we define a strategy that reduces the term to an irreducible form, if any. s t r a t reduce @ LambdaTerm . sd reduce := step ! .

The operator α! executes α until it cannot be further applied. The different implemented strategies for a single reduction are:

-Applicative order (inner rightmost redex first) -By name (normalizing but no reduction inside abstraction)

sd byname := top ( beta ) o re l s e matchrew M N by M u s i n g byname o re l s e matchrew M N by N u s i n g byname .

-By value (only outermost redex and when argument is value)

sd byvalue := ( match (\ x . M ) z | match (\ x . M ) (\ y . N )) ; top ( beta ) .
For example, srew (K I) Omega using applicative does not finish, but srew (K I) Omega using normal produces \ x . x as a result. Moreover, depending on the reduction strategy, we obtain different canonical forms. From (K z) t we get z using all strategies but byvalue, whose canonical form is the term unchanged.

Semantics of programming languages

The semantics of programming languages is an interesting field to apply both strategies [START_REF] Braga | Modular structural operational semantics with strategies[END_REF] and parameterization. The Maude implementation of Eden [START_REF] Hidalgo-Herrero | Using Maude and its strategies for defining a framework for analyzing Eden semantics[END_REF], a concurrent language based on Haskell, can be cited as example. The general idea is that strategies control the execution process and can be used to tweak some semantic choices, and see how alternatives perform. Here we describe a simpler example, the Recursion equations (REC) language [START_REF] Winskel | The Formal Semantics of Programming Languages[END_REF]Chapter 9].

A REC program consists of a closed integer expression to evaluate and a set of integer function definitions of the form f (x 1 , . . . , x a f ) = expr . Expressions contain integer constants, sums, products, subtractions, conditionals, and calls to any defined function. Hence, functions can be recursive and mutually recursive. An organized set of modules (see Figure 3) specifies the representation of REC programs and its basic rules:

r l [ apply ] : Q ( Args ) ⇒ apply ( find (Q , Defs ) , Args ) [ nonexec ] . c r l [ cond ] : if C then E else F ⇒ if C == 0 then E else F fi i f C : Int .
The rule apply replaces a function call Q(Args) by its definition according to the list of definitions Defs, substituting its variables by the call arguments using the equational function apply. This rule is not directly executable since Defs, absent in the left-hand side, must be provided from the context in the application strategy substitution, as we will see. Rule cond resolves a conditional when its condition expression has already been reduced to an integer. In any other case, integer expressions are reduced equationally, since the REC expressions sort RecExpr has been defined as an extension of the built-in sort Int. REC programs are executed following a reduce strategy that receives a list of function definitions as an argument. It is parameterized by a strategy st that is intended to expand function calls, and which we will later instantiate with byvalue and byname alternatives. According to the reduce definition, conditionals and calls are reduced as long as possible, but conditionals are reduced first. This is convenient, since function calls may appear anywhere inside the integer expression, and a simple recursive example like the factorial eq factorial = 'f ( ' n ) := if 'n then 1 else 'n * 'f ( ' n-1 ) .

shows that expanding calls anywhere is problematic. In effect, the precedence of cond avoids the non-terminating reduction 'f(0) → st if 0 then 1 else 0 * 'f(-1) → st if 0 then 1 else 0 * (if -1 then 0 else 'f(-2)) . . . Still, this is not enough when evaluating terms like 'f('f(0)). So, in general, we must ensure not to reduce conditional branches until the condition is solved, no matter if calling by value or by name. To make strategies aware of these precautions while saving code, we will take advantage of strategy parameterization too: we define an additional parameterized module STRAT-EXTENSION that extends a strategy facing function calls st to a strategy xst that applies the reduction step to any program term, but reducing conditions first.

smod STRAT-EXTENSION { X :: REC-STRATEGY } i s s t r a t xst : List { FunctionDef } @ RecExpr . v a r s E F G : RecExpr . Now, the strategy extension is a reusable component that can be used to define the alternative strategies succinctly, avoiding boilerplate code. First, we instantiate STRAT-EXTENSION with views for byname and byvalue, defined in REC-STRATS, to obtain the extended strategies. Then, we instantiate REC-MAIN with new views from REC-STRATEGY to the instantiated modules, mapping st to the extended strategies. On the contrary, the strategy free applies reduction carelessly and anywhere, so it instantiates REC-MAIN directly. The FL parameter must be filled with the program function definitions. For example, with the Ackermann function defined below we execute srew 1 + 'A(2, 3) using reduce(ackermann) . and obtain 10.

eq ackermann = 'A ( 'm , 'n ) := if 'm then 'n + 1 else (if 'n then 'A ( ' m -1 , 1) else 'A ( ' m -1 , 'A ( 'm , 'n -1))) .

eq nameonly = ( ' f ( ' x ) := 'f ( ' x ) + 1) ( ' g ( ' x ) := 7) .

The differences between call by value and call by name are appreciated with the nameonly example, since g(f (0)) will be evaluated to 7 by name while it will never finish by value.

Conclusions

Rewriting strategies are a useful tool in the description of concurrent and logical systems, in accordance with the separation of concerns principle. A stratified specification of rules and its global control allows discharging the functional and rule levels of improper complexity, and makes the specified systems more configurable and adaptable. On the other hand, parameterized modules are a basic feature for building complex systems, reusing abstract specifications, and switching between alternative components. Such specifications can be compared in their multiple instances or analyzed parametrically. The Maude strategy language implementation is now complete, including parameterized strategy modules. In this paper we have seen some examples of parameterized specification with strategies related to algorithms and programming languages. In the future, the combination of strategies and parameterization can be used as a fundamental approach to specify more complex and interesting systems. Also, more elaborated analyses can be done on these, including model checking, whose strategy-aware implementation is currently under development.

  Maude > srew f ( g ( f ( a ) , b )) using pf . Solution 1 result Term : g ( f ( a ) , b ) Solution 2 result Term : f ( g (a , b )) No more solutions . Maude > srew f ( g ( f ( a ) , b )) using pf [ T <-a ] . Solution 1 result Term : f ( g (a , b )) No more solutions .

  Solution 1 result Term : g (d , c ) Solution 2 result Term : g (c , c ) No more solutions .

Fig. 1 .

 1 Fig. 1. Strategic set-theoretic semantics definitions

Fig. 2 .

 2 Fig. 2. Module structure for the simplex algorithm specification

  sd step := ( unbounded | finish | phase2 | unfeas ) o re l s e pivotingStrat .

K

  = λx.(λy.x) I = λx.x Ω = (λx.xx)(λx.xx)

-

  sd applicative := matchrew \ x . M by M u s i n g applicative | matchrew M N by N u s i n g applicative o re l s e matchrew M N by M u s i n g applicative o re l s e top ( beta ) . Normalizing strategy (outer leftmost redex first) sd normal := matchrew \ x . M by M u s i n g normal | top ( beta ) o re l s e matchrew M N by M u s i n g normal o re l s e matchrew M N by N u s i n g normal .

Fig. 3 .

 3 Fig. 3. Module structure for the REC language specification

v a r FL :

 FL List { FunctionDef } . sd xst ( FL ) := st ( FL ) | matchrew E + F by E u s i n g xst ( FL ) o re l s e matchrew E + F by F u s i n g xst ( FL ) | matchrew E * F by E u s i n g xst ( FL ) o re l s e matchrew E * F by F u s i n g xst ( FL ) | ( matchrew E -F by E u s i n g xst ( FL )) o re l s e matchrew E -F by F u s i n g xst ( FL ) | matchrew if E then F else G by E u s i n g xst ( FL ) . endsm

  sd free ( FL ) := apply [ Defs <-FL ] . sd byname ( FL ) := top ( apply [ Defs <-FL ]) . sd byvalue ( FL ) := ( matchrew E , NeArgs by E u s i n g byvalue ( FL )) o re l s e matchrew E , NeArgs by NeArgs u s i n g byvalue ( FL ) | ( matchrew Q ( Args ) by Args u s i n g byvalue ( FL )) o re l s e top ( apply [ Defs <-FL ]) .

  Functional modules are bound to some executability requirements, like confluence, termination, and sort-decreasingness.

	fmod INT-SET i s
	p r o t e c t i n g INT .	*** INT module importation
	s o r t IntSet .
	s u b s o r t Int < IntSet .
	*** IntSet contructors ( ctor )
	op empty : → IntSet [ ctor ] .
	op __ : IntSet IntSet → IntSet
	[ ctor assoc comm id : empty ] . *** union
	v a r X : Int .
	eq X X = X .
	endfm

  rules are required to be coherent with equations and axioms[7, §5.3]. Conditions of the third type are called rewriting conditions, and hold true iff the term w k can be rewritten to match the term w k .

mod SUM-SET i s p r o t e c t i n g INT-SET . v a r s X Y : Int . r l [ sum ] : X Y ⇒ X + Y . *** matches any two elems endm

  The following module specifies the search for a Hamiltonian cycle in a graph, i.e. a cycle visiting every vertex of the graph only once.

mod HAMILTONIAN i s p r o t e c t i n g LIST { Nat } . s o r t s Edge Adjacency Graph . s u b s o r t Edge < Adjacency . op e : Nat Nat → Edge [ ctor comm ] . op nil : → Adjacency [ ctor ] . op __ : Adjacency Adjacency → Adjacency [ ctor assoc comm id : nil ] . op noCross : List { Nat } → Bool . v a r s K L N V : Nat . v a r s P Q R : List { Nat } . v a r As : Adjacency . eq noCross ( P K Q K R ) = false . eq noCross ( P ) = true [ owise ] . op graph : Nat Adjacency List { Nat } → Graph [ ctor ] . op isOk : Graph → Bool . op isSolution : Graph → Bool .

  e w HamiltonianBT from BT-ELEMS t o HAMILTONIAN i s s o r t State t o Graph . op isOk to isOk . op isSolution to isSolution . strat expand to-expr next . endv

Research partially supported by MCIU Spanish project TRACES (TIN2015-67522-C3-3-R), and by Comunidad de Madrid project N-Greens Software-CM (S2013/ICE-2731).


Mathieu Colin

Tatsuo Iguchi

Solitary wave solutions to the Isobe-Kakinuma model for water waves

We consider the Isobe-Kakinuma model for two-dimensional water waves in the case of the flat bottom. The Isobe-Kakinuma model is a system of Euler-Lagrange equations for a Lagrangian approximating Luke's Lagrangian for water waves. We show theoretically the existence of a family of small amplitude solitary wave solutions to the Isobe-Kakinuma model in the long wave regime. Numerical analysis for large amplitude solitary wave solutions is also provided and suggests the existence of a solitary wave of extreme form with a sharp crest.

Introduction

In this paper we consider the motion of two-dimensional water waves in the case of the flat bottom. The water wave problem is mathematically formulated as a free boundary problem for an irrotational flow of an inviscid and incompressible fluid under the gravitational field. Let t be the time and (x, z) the spatial coordinates. We assume that the water surface and the bottom are represented as z = η(x, t) and z = -h, respectively. As was shown by J. C. Luke [START_REF] Luke | A variational principle for a fluid with a free surface[END_REF], the water wave problem has a variational structure. His Lagrangian density is of the form where Φ = Φ(x, z, t) is the velocity potential and g is the gravitational constant. M. Isobe [START_REF] Isobe | A proposal on a nonlinear gentle slope wave equation[END_REF][START_REF] Isobe | Time-dependent mild-slope equations for random waves[END_REF] and T. Kakinuma [START_REF] Kakinuma | [END_REF][START_REF] Kakinuma | A set of fully nonlinear equations for surface and internal gravity waves[END_REF][START_REF] Kakinuma | A nonlinear numerical model for surface and internal waves shoaling on a permeable beach[END_REF] proposed a model for water waves as a system of Euler-Lagrange equations for an approximate Lagrangian, which is derived from Luke's Lagrangian by approximating the velocity potential Φ in the Lagrangian appropriately. In this paper, we adopt an approximation under the form

(1.2) Φ(x, z, t) ≃ N i=0 (z + h) p i φ i (x, t),
where p 0 , p 1 , . . . , p N are nonnegative integers satisfying 0 = p 0 < p 1 < • • • < p N . Then, the corresponding Isobe-Kakinuma model in a nondimensional form is written as

(1.3)                    H p i ∂ t η + N j=0 ∂ x 1 p i + p j + 1
H p i +p j +1 ∂ x φ jδ -2 p i p j p i + p j -1 H p i +p j -1 φ j = 0 for i = 0, 1, . . . , N,

N j=0 H p j ∂ t φ j + η + 1 2      N j=0 H p j ∂ x φ j   2 + δ -2   N j=0 p j H p j -1 φ j   2    = 0,
where H(x, t) = 1 + η(x, t) is the normalized depth of the water and δ a nondimensional parameter defined by the ratio of the mean depth h to the typical wavelength λ. Here and in what 1 follows we use the notational convention 0 0 = 0. For the derivation and basic properties of this model, we refer to Y. Murakami and T. Iguchi [START_REF] Murakami | Solvability of the initial value problem to a model system for water waves[END_REF] and R. Nemoto and T. Iguchi [START_REF] Nemoto | Solvability of the initial value problem to the Isobe-Kakinuma model for water waves[END_REF]. Moreover, it was shown by T. Iguchi [START_REF] Iguchi | Isobe-Kakinuma model for water waves as a higher order shallow water approximation[END_REF][START_REF] Iguchi | A mathematical justification of the Isobe-Kakinuma model for water waves with and without bottom topography[END_REF] that the Isobe-Kakinuma model (1.3) is a higher order shallow water approximation for the water wave problem in the strongly nonlinear regime. We note also that the Isobe-Kakinuma model (1.3) in the case N = 0 is exactly the same as the shallow water equations. In the sequel, we always assume N ≥ 1.

In this paper, we look for solitary wave solutions to this model under the form (1.4) η = η(x + ct), φ j = φ j (x + ct), j = 0, 1, . . . , N, where c ∈ R is an unknown constant phase speed. Plugging (1.4) into (1.3), we obtain a system of ordinary differential equations (1.5)

                   cH p i η ′ + N j=0 1 p i + p j + 1 H p i +p j +1 φ ′ j ′ -δ -2 p i p j p i + p j -1
H p i +p j -1 φ j = 0 for i = 0, 1, . . . , N, c N j=0

H p j φ ′ j + η + 1 2      N j=0 H p j φ ′ j   2 + δ -2   N j=0 p j H p j -1 φ j   2    = 0.
As expected, this system has a variational structure, that is, the solution of this system is obtained as a critical point of the functional L IK (φ 0 , . . . , φ N , η) = cM IK (φ 0 , . . . , φ N , η) + E IK (φ 0 , . . . , φ N , η), where M IK (φ 0 , . . . , φ N , η) = R η(x)∂ x Φ app (x, η(x)) dx,

E IK (φ 0 , . . . , φ N , η) = 1 2 R η(x) -1 (∂ x Φ app (x, z)) 2 + (δ -1 ∂ z Φ app (x, z)) 2 dz + η(x) 2 dx,
and Φ app is the approximate velocity potential defined by

Φ app (x, z) = N i=0
(z + 1) p i φ i (x, t).

We note that M IK and E IK represent the momentum in the horizontal direction and the total energy of the water, respectively. Both of them are conserved quantities for the Isobe-Kakinuma model (1.3). In this paper we do not use this variational structure to construct solitary wave solutions to the Isobe-Kakinuma model, whereas we use a perturbation method with respect to the small nondimensional parameter δ in the long wave regime.

In order to give one of our main results in this paper concerning the existence of a family of solutions to (1.5), we introduce norms • and • k for k = 0, 1, 2, . . . , by (1.6) u = sup

x∈R e |x| |u(x)|, u k = k j=0 u (j) ,
where u (j) is the j-th order derivative of u. We also introduce the function spaces B k e and B k o as closed subspaces of all even and odd functions u ∈ C k (R) satisfying u k < +∞, respectively, equipped with the norm • k , and put

B ∞ α = ∩ ∞ k=0 B k α for α = e, o.
The following theorem guarantees the existence of small amplitude solitary wave solutions to the Isobe-Kakinuma model in the long wave regime.

Theorem 1.1. There exists a positive constant δ 0 such that for any δ ∈ (0, δ 0 ] the Isobe-Kakinuma model (1.5) has a solution (c δ , η δ , φ δ 0 , . . . , φ δ N ), which satisfies η δ , φ δ′ 0 ∈ B ∞ e and φ δ 1 , . . . , φ δ N ∈ B ∞ o . Moreover, the solution satisfies c δ = 1 + 2γδ 2 and

η δ -4γδ 2 sech 2 x k + (φ δ 0 + 4γδ 2 tanh x) ′ k ≤ C k δ 4 , φ δ j -4γγ j δ 4 sech 2 x tanh x k ≤ C k δ 6 for j = 1, . . . , N
for any k ∈ N, where the constants γ, γ 1 , . . . , γ N are determined through p 1 , . . . , p N and the constant C k does not depend on δ but on k.

Remark 1.2. The constants γ and γ = (γ 1 , . . . , γ N ) T in the statement of Theorem 1.1 are given by γ

= A -1 1 (1 -a 0 ) and γ = (1 -a 0 ) • A -1 1 (1 -a 0 )
with a N × N matrix A 1 and a vector a 0 given by

(1.7) A 1 = p i p j p i + p j -1 1≤i,j≤N , 1 a T 0 a 0 A 0 = 1 p i + p j + 1 0≤i,j≤N
, and 1 = (1, . . . , 1) T . The matrices A 0 and A 1 are positive, so that the constant γ is also positive. We will use these notations throughout this paper.

Remark 1.3. This theorem ensures the existence of a family of solitary wave solutions to the Isobe-Kakinuma model traveling to the left. We can also show a similar existence theorem to solitary wave solutions to the model traveling to the right.

Remark 1.4. By neglecting the term of order O(δ 4 ), the solitary wave solutions in the dimensional form are given by

             c ≃ 1 + a 2h √ gh, η(x, t) ≃ a sech 2 a 4γh 3 (x + ct) , φ 0 (x, t) ≃ -4γgah 2 tanh a 4γh 3 (x + ct) , φ j (x, t) ≃ 0 for j = 1, . . . , N,
where g is the gravitational constant and a is the amplitude of the wave.

In this paper we also analyze numerically the existence of large amplitude solitary wave solutions to the Isobe-Kakinuma model in a special case where we choose the parameters as N = 1 and p 1 = 2, that is, (7.1). We note that even in this simplest case the Isobe-Kakinuma model gives a better approximation than the well-known Green-Naghdi equations in the shallow water and strongly nonlinear regime. See T. Iguchi [START_REF] Iguchi | Isobe-Kakinuma model for water waves as a higher order shallow water approximation[END_REF][START_REF] Iguchi | A mathematical justification of the Isobe-Kakinuma model for water waves with and without bottom topography[END_REF]. Numerical analysis suggests that there exists a critical value of δ given approximately by (1.8) δ c = 0.62633493 such that for any δ ∈ (0, δ c ), the Isobe-Kakinuma model (7.1) admits a smooth solitary wave solution and that this family of waves converges to a solitary one of extreme form with a shape crest as δ ↑ δ c . Moreover, the included angle θ of the crest in the physical space is given approximately by (1.9) θ = 152.6 • . Here, we mention the related results on the existence of the solitary wave solutions to the water wave problem. The existence of small amplitude solitary waves for the water wave problem was first given by K. O. Friedrichs and D. H. Hyers [START_REF] Friedrichs | The existence of solitary waves[END_REF]. Then, C. J. Amick and J. F. Toland [START_REF] Amick | On solitary water-waves of finite amplitude[END_REF] proved the existence of solitary wave solutions of all amplitudes from zero up to and including that of the solitary wave of greatest height. On the other hand, a periodic wave of permanent form is called Stokes' wave. The existence of Stokes's wave of extreme form as well as the sharp crest of the included angle 120 • was predicted by G. G. Stokes [START_REF] Stokes | On the theory of oscillatory waves[END_REF], and then proved theoretically by C. J. Amick, L. E. Fraenkel, and J. F. Toland [START_REF] Amick | On the Stokes conjecture for the wave of extreme form[END_REF]. An extension of these existence theories to the water waves with vorticity was given by E. Varvaruca [START_REF] Varvaruca | On the existence of extreme waves and the Stokes conjecture with vorticity[END_REF]. The author has proved the existence of the solitary wave as well as Stokes' wave of greatest height with a shape crest of the same included angle 120 • as in the irrotational case. As for the model equations for water waves, it is well-known that the Korteweg-de Vries equation has solitary wave solutions of arbitrarily large amplitude and does not have any wave of extreme form. The Green-Naghdi equations are known as higher order shallow water approximate equations for water waves in the strongly nonlinear regime and have the same solitary wave solutions as those of the Korteweg-de Vries equation, but again does not have any solitary wave of extreme form. Compared to these models, the Isobe-Kakinuma model even in the simplest case catches the property on the existence of the solitary wave of extreme form, although the included angle of the crest is not 120 • . We also mention a result by D. Lannes and F. Marche [START_REF] Lannes | Nonlinear wave-current interactions in shallow water[END_REF], where it was shown that an extended Green-Naghdi equations for the water waves with a constant vorticity has a solitary wave solution of extreme form.

See

The contents of this paper are as follows. In Section 2, we give conservation laws for the Isobe-Kakinuma model, which will be used in the numerical analysis in Section 7. In Section 3, by using formal asymptotic analysis we calculate the first order approximate term with respect to δ 2 in the expansion (3.2) of the solitary wave solution to the Isobe-Kakinuma model (1.5). In Section 4, we reduce the problem by deriving equations for the remainder terms. In Section 5, we construct Green's functions for the linearized equations together with their estimates. In Section 6, we first prove an existence theorem for the system of linear equations derived in Section 4 and then prove the existence of small amplitude solitary wave solutions to the Isobe-Kakinuma model. Finally, in Section 7, we analyze numerically large amplitude solitary wave solutions and calculate the solitary wave of extreme form together with the included angle.

As was explained in the previous section, for the Isobe-Kakinuma model (1.3), the mass, the momentum in the horizontal direction, and the total energy are conserved. In the numerical analysis which will be carried out in Section 7, we also need to know corresponding flux functions. The following proposition gives such flux functions. Proposition 2.1. Any regular solution (η, φ 0 , . . . , φ N ) to the Isobe-Kakinuma model (1.3) satisfies the conservation laws

(2.1) ∂ t η + ∂ x   N j=0 1 p j + 1 H p j+1 ∂ x φ j   = 0, ∂ t η∂ x N i=0 H p i φ i + ∂ x -η∂ t N i=0 H p i φ i - 1 2 η 2 (2.2) + 1 2 N i,j=0 1 p i + p j + 1 H p i +p j +1 (∂ x φ i )(∂ x φ j ) -δ -2 p i p j p i + p j -1 H p i +p j -1 φ i φ j    = 0, and
∂ t    1 2 η 2 + 1 2 N i,j=0 1
p i + p j + 1 H p i +p j +1 (∂ x φ i )(∂ x φ j ) + δ -2 p i p j p i + p j -1 H p i +p j -1 φ i φ j    (2.3) -∂ x    N i,j 1 p i + p j + 1 H p i +p j +1 (∂ x φ i )(∂ t φ j )    = 0.
Proof. Conservation law of mass (2.1) is nothing but the first equation in (1.3) with i = 0. It follows from the equations in (1.3) that

∂ t η∂ x N i=0 H p i φ i -∂ x η∂ t N i=0 H p i φ i = (∂ t η) N i=0 H p i ∂ x φ i -(∂ x η) N i=0 H p i ∂ t φ i = N i=0   - N j=0 ∂ x 1 p i + p j + 1 H p i +p j +1 ∂ x φ j -δ -2 p i p j p i + p j -1 H p i +p j -1 φ j   ∂ x φ i + (∂ x η)   η + 1 2      N j=0 H p j ∂ x φ j   2 + δ -2   N j=0 p j H p j -1 φ j   2      = - N i,j=0 1
p i + p j + 1 H p i +p j +1 (∂ x φ i )(∂ 2 x φ j ) -δ -2 p i p j p i + p j -1 H p i +p j -1 φ j ∂ x φ i + (∂ x η)    η - 1 2 N i,j=0 H p i +p j (∂ x φ i )(∂ x φ j ) -δ -2 p i p j H p i +p j -2 φ i φ j    = ∂ x    1 2 η 2 - 1 2 N i,j=0 1 p i + p j + 1 H p i +p j +1 (∂ x φ i )(∂ x φ j ) -δ -2 p i p j p i + p j -1 H p i +p j -1 φ i φ j    ,
which gives conservation law of momentum (2.2). We see also that

∂ t    1 2 η 2 + 1 2 N i,j=0 1
p i + p j + 1 H p i +p j +1 (∂ x φ i )(∂ x φ j ) + δ -2 p i p j p i + p j -1 H p i +p j -1 φ i φ j    = (∂ t η)   η + 1 2      N j=0 H p j ∂ x φ j   2 + δ -2   N j=0 p j H p j -1 φ j   2      + N i,j=0 1 p i + p j + 1 H p i +p j +1 (∂ x φ i )(∂ t ∂ x φ j ) + δ -2 p i p j p i + p j -1 H p i +p j -1 φ i ∂ t φ j = -(∂ t η) N j=0 H p j ∂ t φ j + ∂ x    N i,j=0 1
p i + p j + 1 H p i +p j +1 (∂ x φ i )(∂ t φ j )    + N i,j=0 ∂ x 1 p i + p j + 1 H p i +p j +1 ∂ x φ i -δ -2 p i p j p i + p j -1 H p i +p j -1 φ i ∂ t φ j = ∂ x    N i,j=0 1 p i + p j + 1 H p i +p j +1 (∂ x φ i )(∂ t φ j )    ,
which gives conservation law of energy (2.3).

These conservation laws provide directly the following proposition.

Proposition 2.2. For any regular solution (η, φ 0 , . . . , φ N ) to the Isobe-Kakinuma model (1.5) satisfying the condition at spatial infinity

(2.4) η(x), φ ′ 0 (x), . . . , φ ′ N (x), φ 1 (x), . . . , φ N (x) → 0 as x → ±∞,
we have

(2.5) cη + N j=0 1 p j + 1 H p j +1 φ ′ j = 0 and (2.6) 1 2 η 2 - 1 2 N i,j=0 1
p i + p j + 1 H p i +p j +1 φ ′ i φ ′ j -δ -2 p i p j p i + p j -1 H p i +p j -1 φ i φ j = 0.

Approximate solutions

We first transform the Isobe-Kakinuma model (1.5) into an equivalent system. The first equation in (1.5) with i = 0 can be integrated under the condition at spatial infinity (2.4) so that we have (2.5), particularly,

cη = - N j=0 1 p j + 1 H p j +1 φ ′ j .
Plugging this into the first equation in (1.5) with i = 1, . . . , N to eliminate cη, we have

H p i N j=0 1 p j + 1 H p j +1 φ ′ j ′ = N j=0 1 p i + p j + 1 H p i +p j +1 φ ′ j ′ -δ -2 p i p j p i + p j -1 H p i +p j -1 φ j , which are equivalent to N j=0 1 p j + 1 - 1 p i + p j + 1 H p j +2 φ ′′ j + δ -2 N j=0 p i p j p i + p j -1 H p j φ j = 0 for i = 1, . . . , N . Therefore, (1.5) under the condition (2.4) is transformed equivalently into (3.1)                              cη + N j=0 1 p j + 1 H p j +1 φ ′ j = 0, N j=0 1 p j + 1 - 1 p i + p j + 1 H p j +2 φ ′′ j + δ -2 N j=0 p i p j p i + p j -1 H p j φ j = 0 for i = 1, . . . , N, c N j=0 H p j φ ′ j + η + 1 2      N j=0 H p j φ ′ j   2 + δ -2   N j=0 p j H p j -1 φ j   2    = 0,
where H = 1 + η.

To simplify the notation, we put φ = (φ 1 , . . . , φ N ) T . Suppose that (c, η, φ 0 , φ) is a solution to (3.1) and can be expanded with respect to δ 2 as

(3.2)            c = c (0) + δ 2 c (1) + δ 4 c (2) + • • • , η = δ 2 (η (0) + δ 2 η (1) + δ 4 η (2) + • • • ), φ 0 = δ 2 (φ 0(0) + δ 2 φ 0(1) + δ 4 φ 0(2) + • • • ), φ = δ 2 (φ (0) + δ 2 φ (1) + δ 4 φ (2) + • • • ).
Remark 3.1. In this expansion, we assumed a priori that η, φ 0 , and φ are of order O(δ 2 ). This is essentially the assumption that the solution is in the long wave regime.

Then, equating the coefficients of the lowest power of δ 2 we have A 1 φ (0) = 0 so that φ (0) = 0, because A 1 is nonsingular. Equating the coefficients of δ 2 we have

       c (0) η (0) + φ ′ 0(0) = 0, (1 -a 0 )φ ′′ 0(0) + A 1 φ (1) = 0, c (0) φ ′ 0(0) + η (0) = 0.
It follows from the first and the third equations of the above system that c 2 (0) = 1 in order to obtain a nontrivial solution. In the following we will consider the case c (0) = 1. Then, we have

(3.3) φ ′ 0(0) = -η (0) , φ (1) = -γφ ′′ 0(0) = γη ′ (0)
, where γ is the constant vector defined in Remark 1.2. Next, equating the coefficients of δ 4 in the first and the third equations in (3.1) we have

η (1) + φ ′ 0(1) + c (1) η (0) + η (0) φ ′ 0(0) + a 0 • φ ′ (1) = 0, φ ′ 0(1) + η (1) + c (1) φ ′ 0(0) + 1 • φ ′ (1) + 1 2 (φ ′ 0(0) ) 2 = 0, which together with (3.3) yield (3.4) 2c (1) η (0) - 3 2 η 2 (0) -γη ′′ (0) = 0,
where γ is the positive constant defined in Remark 1.2.

As is well known, (3.4) has a family of solutions of the form

c (1) = α, η (0) (x) = 2α sech 2 α 2γ x
with a parameter α > 0. Then, it follows from (3.3) that

   φ 0(0) (x) = -2 √ 2αγ tanh α 2γ x + const., φ (1) (x) = -4αγ α 2γ tanh α 2γ x sech 2 α 2γ x .
Therefore, it is natural to expect that (1.5) has a family of solutions of the form

(3.5)              c = 1 + αδ 2 + O(δ 4 ), η(x) = 2αδ 2 sech 2 α 2γ x + O(δ 4 ), φ 0 (x) = -2 √ 2αγδ 2 tanh α 2γ x + O(δ 4 ), φ(x) = -4αγ α 2γ δ 4 tanh α 2γ x sech 2 α 2γ x + O(δ 6 )
with parameters α > 0 and 0 < δ ≪ 1.

Reduction of the problem

Without loss of generality, we can assume that α = 2γ. We denote the approximate solitary wave solution obtained in the previous section by η (0) and φ (0) , that is,

(4.1) η (0) (x) = 4γ sech 2 x, φ (0) (x) = -4γ tanh x.
Then, we will look for solutions to the Isobe-Kakinuma model (1.5) in the form

(4.2) c = 1 + 2γδ 2 , η = δ 2 η (0) + δ 4 ζ, φ 0 = δ 2 φ (0) + δ 4 ψ 0 , φ = δ 4 γη ′ (0) + δ 6 ψ.
Plugging these into the first and the third equations in (3.1) we obtain

(4.3) ζ + ψ ′ 0 + G 1 + δ 2 (2γ -η (0) )ζ + η (0) ψ ′ 0 + a 0 • ψ ′ + G 2 + δ 4 F 1 = 0, ζ + ψ ′ 0 + G 3 + δ 2 (2γ -η (0) )ψ ′ 0 + 1 • ψ ′ + G 4 + δ 4 F 2 = 0, where            G 1 = 2γη (0) -η 2 (0) + κ 1 η ′′ (0) , G 2 = κ 2 η (0) η ′′ (0) , G 3 = -2γη (0) + 1 2 η 2 (0) + κ 2 η ′′ (0) , G 4 = κ 2 (2γ -η (0) )η ′′ (0) + κ 3 η (0) η ′′ (0) + 1 2 κ 2 3 (η ′ (0) ) 2 , with κ 1 = a 0 • γ, κ 2 = 1 • γ, and κ 3 = (p 1 , . . . , p N ) T • γ and F 1 = ζψ ′ 0 + η (0) N j=1 ψ ′ j + N j=1 1 p j + 1 δ -4 H p j +1 -1 -δ 2 (p j + 1)η (0) (γ j η ′′ (0) + δ 2 ψ ′ j ), F 2 = F 3 + 2γF 4 + 1 2 (ψ ′ 0 + κ 2 η ′′ (0) ) 2 + 1 2 δ -4 φ ′ (0) + δ 2 (ψ ′ 0 + κ 2 η ′′ (0) ) + δ 4 F 4 2 -φ ′ (0) + δ 2 (ψ ′ 0 + κ 2 η ′′ (0) ) 2 + 1 2 δ -2      N j=1 p j H p j -1 (γ j η ′ (0) + δ 2 ψ j )   2 -   N j=1 p j γ j η ′ (0)   2    , with H = 1 + δ 2 η (0) + δ 4 ζ and F 3 = η (0) N j=1 p j ψ ′ j + N j=1 δ -4 (H p j -1 -δ 2 p j η (0) )(γ j η ′′ (0) + δ 2 ψ ′ j ), F 4 = N j=1 ψ ′ j + N j=1 δ -2 (H p j -1)(γ j η ′′ (0) + δ 2 ψ ′ j ).
In the above calculations, we have used the identities

N j=0 H p j φ ′ j = δ 2 φ ′ (0) + δ 4 (ψ ′ 0 + κ 2 η ′′ (0) ) + δ 6   κ 3 η (0) η ′′ (0) + N j=1 ψ ′ j   + δ 8 F 3 = δ 2 φ ′ (0) + δ 4 (ψ ′ 0 + κ 2 η ′′ (0) ) + δ 6 F 4 .
Since η (0) satisfies (3.4) with c (1) = 2γ, we have G 1 = G 3 , so that (4.3) is equivalent to

(4.4) (η (0) -2γ)ζ + 2(γ -η (0) )ψ ′ 0 + (1 -a 0 ) • ψ ′ = g 0 + δ 2 f 0 , ζ + ψ ′ 0 = g N +1 + δ 2 f N +1 , with g 0 = G 2 -G 4 , g N +1 = G 1 , f 0 = F 1 -F 2 , and f N +1 = (η (0) -2γ)ψ ′ 0 -1 • ψ ′ -G 4 -δ 2 F 2 .
On the other hand, plugging (4.2) into the second equation in (3.1), we obtain

(4.5) (1 -a 0 )ψ ′′ 0 -δ 2 (A 0 -1 ⊗ a 0 )ψ ′′ + A 1 ψ = g + δ 2 f ,
where

g = 2(1 -a 0 ) -A 1 diag(p 1 , . . . , p N )γ η (0) η ′ (0) + (A 0 -1 ⊗ a 0 )γη ′′′ (0) , (4.6) f = (1 -a 0 ) δ -4 (H 2 -1 -2δ 2 η (0) )η ′ (0) + δ -2 (H 2 -1)ψ ′′ 0 (4.7) -(A 0 -1 ⊗ a 0 )δ -2 diag(H p 1 +2 -1, . . . , H p N +2 -1) (γη ′′′ (0) + δ 2 ψ ′′ ) -A 1 δ -4 diag(H p 1 -1 -δ 2 p 1 η (0) , . . . , H p N -1 -δ 2 p N η (0) ) γη ′ (0) + δ -2 diag(H p 1 -1, . . . , H p N -1) ψ .
To summarize, the Isobe-Kakinuma model (3.1) is reduced to

(4.8)      (η (0) -2γ)ζ + 2(γ -η (0) )ψ ′ 0 + (1 -a 0 ) • ψ ′ = g 0 + δ 2 f 0 , (1 -a 0 )ψ ′′ 0 -δ 2 (A 0 -1 ⊗ a 0 )ψ ′′ + A 1 ψ = g + δ 2 f , ζ + ψ ′ 0 = g N +1 + δ 2 f N +1
for the remainder terms (ζ, ψ 0 , ψ). We note that g 0 and g N +1 are polynomials in (η (0) , η ′ (0) , η ′′ (0) ), that g is a polynomial in (η (0) , η ′ (0) , η ′′′ (0) ), and that g 0 , g N +1 ∈ B ∞ e and g ∈ B ∞ o . Moreover, f 0 and f N +1 are polynomials in (η (0) , η ′ (0) , η ′′ (0) , ζ, ψ ′ 0 , ψ, ψ ′ ), and f is a polynomial in (η (0) , η ′ (0) , η ′′′ (0) , ζ, ψ ′′ 0 , ψ, δ 2 ψ ′′ ), whose coefficients are polynomials in δ. In view of (4.8) we proceed to consider the following system of linear ordinary differential equations (4.9)

     (η (0) -2γ)ζ + 2(γ -η (0) )ψ ′ 0 + (1 -a 0 ) • ψ ′ = F 0 , (1 -a 0 )ψ ′′ 0 -δ 2 (A 0 -1 ⊗ a 0 )ψ ′′ + A 1 ψ = F , ζ + ψ ′ 0 = F N +1
for unknowns (ζ, ψ 0 , ψ). We can rewrite the third equation in (4.9) as

(4.10) ζ = -ψ ′ 0 + F N +1 ,
which enable us to remove the unknown variable ζ from the equations. It follows from the second equations in (4.9) that

ψ = -γψ ′′ 0 + δ 2 A 2 ψ ′′ + A -1 1 F , where A 2 = A -1 1 (A 0 -1 ⊗ a 0 )
. Plugging this and (4.10) into the first equation in (4.9), we obtain (4.11)

-γψ ′′′ 0 + (4γ -3η (0) )ψ ′ 0 = F 0 + (2γ -η (0) )F N +1 -γ • F ′ -δ 2 β • ψ ′′′ , 10
where β = A T 2 (1a 0 ). This is the equation for ψ 0 . In order to derive equations to solve ψ, we put χ = ψ ′′ 0 . Then, it follows from (4.9) that

(4.12) (1 -a 0 ) • ψ ′ = F 0 + (2γ -η (0) )F N +1 + (3η (0) -4γ)ψ ′ 0 , (1 -a 0 )χ -δ 2 (A 0 -1 ⊗ a 0 )ψ ′′ + A 1 ψ = F ,
This is the equations for (χ, ψ). Of course, χ is expected to be ψ ′′ 0 , but we do not know it a priori. However, we have the following lemma. Proof. It follows from the second equation in (4.12) that

ψ = -γχ + δ 2 A 2 ψ ′′ + A -1 1 F .
Plugging this into the first equation in (4.12) we have

-γχ ′ + (4γ -3η (0) )ψ ′ 0 = F 0 + (2γ -η (0) )F N +1 -γ • F ′ -δ 2 β • ψ ′′′ .
Comparing this with (4.11) we obtain (χψ ′′ 0 ) ′ = 0, which gives the desired results.

Green's functions

In view of (4.11), we first consider the solvability of the equation for an unknown u

(5.1)

-γu ′′ + (4γ -3η (0) )u = f
under the condition u(x) → 0 as x → ±∞. We remind that η (0) (x) = 4γ sech 2 x, so that this equation does not depend essentially on the positive constant γ. This equation has already been analyzed by K. O. Friedrichs and D. H. Hyers [START_REF] Friedrichs | The existence of solitary waves[END_REF]. Let us recall briefly their result. In order to construct Green's function, we consider the initial value problems with homogeneous equation:

-γu ′′ 1 + (4γ -3η (0) )u 1 = 0, u 1 (0) = 0, u ′ 1 (0) = 1, -γu ′′ 2 + (4γ -3η (0) )u 2 = 0, u 2 (0) = 1, u ′ 2 (0) = 0.
The solutions of these initial value problems have the form

u 1 (x) = sech 2 x tanh x, u 2 (x) = 1 8 (-6 -cosh(2x) + 15sech 2 x -15xsech 2 x tanh x).
We note that these fundamental solutions satisfy

(5.2) |u (k) 1 (x)| ≤ C k e -2|x| , |u (k) 2 (x)| ≤ C k e 2|x|
for k = 0, 1, 2, . . .. Since the Wronskian is u ′ 1 (x)u 2 (x)u 1 (x)u ′ 2 (x) ≡ 1, the solution u of (5.1) can be written as

u(x) = γ -1 C 1 - x 0 u 2 (y)f (y)dy u 1 (x) + γ -1 C 2 + x 0 u 1 (y)f (y)dy u 2 (x),
where C 1 and C 2 are arbitrary constants. In order that this solution satisfies the condition u(x) → 0 as x → ±∞, as necessary conditions, we obtain

C 2 + ∞ 0 u 1 (y)f (y)dy = C 2 - 0 -∞
u 1 (y)f (y)dy = 0, so that we have a necessary condition

(5.3) ∞ -∞ u 1 (y)f (y)dy = 0
for the existence of the solution, and that the solution has the form

u(x) = γ -1 u 1 (x) C 1 - x 0 u 2 (y)f (y)dy -γ -1 u 2 (x) ∞ x u 1 (y)f (y)dy.
Nonuniqueness of the solution comes from the translation invariance of the original equations.

Proposition 5.1. Let γ > 0. For any f ∈ B ∞ e , there exists a unique solution u ∈ B ∞ e to (5.1). Moreover, for any k = 0, 1, 2, . . ., the solution satisfies

u k+2 ≤ C 0 f k + C k f 0 ,
where C k is a positive constant depending on k while C 0 does not.

Proof. Since f is even and u 1 is odd, the necessary condition (5.3) for the existence of the solution is automatically satisfied. Moreover, we restricted ourselves to a class of solutions which are even so that the solution is unique and given by

u(x) = -γ -1 u 1 (x) x 0 u 2 (y)f (y)dy -γ -1 u 2 (x) ∞ x u 1 (y)f (y)dy.
Using this solution formula, we easily obtain u k+2 ≤ C k f k .

We proceed to improve this estimate. Differentiating (5.1) j-times, we have -γu (j)′′ + (4γ -3η (0) )u (j) = f (j) + 3[( d dx ) j , η (0) ]u Applying the previous estimate with k = 0 to u (j) and adding them for j = 1, 2, . . . , k, we obtain

u k+2 ≤ C f k + C k u W k,∞ , which together with the interpolation inequality u W k,∞ ≤ ǫ u W k+2,∞ + C ǫ u L ∞ ≤ ǫ u k+2 + C ǫ u 2 for
any ǫ > 0 yields the refined estimate.

In view of (4.12), we then consider the solvability of the system of ordinary differential equations with constant coefficients

(5.4) (1 -a 0 ) • ϕ = f 0 , (1 -a 0 )ϕ 0 -δ 2 (A 0 -1 ⊗ a 0 )ϕ ′′ + A 1 ϕ = f ,
for unknowns ϕ 0 and ϕ = (ϕ 1 , . . . , ϕ N ) T while f 0 and f = (f 1 , . . . , f N ) T are given functions. We procced to construct Green's function to this system. By taking the Fourier transform of (5.4), we obtain 0 (1

-a 0 ) T 1 -a 0 (δξ) 2 (A 0 -1 ⊗ a 0 ) + A 1 φ0 φ = f0 f .
Now, we need to show that the coefficient matrix is invertible. Put (5.5)

q(ξ 2 ) = -det 0 (1 -a 0 ) T 1 -a 0 ξ 2 (A 0 -1 ⊗ a 0 ) + A 1 .
Then, we have the following lemma.

Lemma 5.2. q(ξ 2 ) is a polynomial in ξ 2 of degree N -1. Moreover, there exists a positive constant c 0 such that for any ξ ∈ R we have q(ξ 2 ) ≥ c 0 > 0.

Proof. It is easy to see that

q(ξ 2 ) = -det 0 (1 -a 0 ) T 1 -a 0 ξ 2 (A 0 -a 0 ⊗ a 0 ) + A 1 .
Here, we will show that the symmetric matrix A 0a 0 ⊗ a 0 is positive. In fact, for any φ = (φ 1 , . . . , φ N ) T ∈ R N , we see that

φ • (A 0 -a 0 ⊗ a 0 )φ = N i,j=1 1
p i + p j + 1 φ i φ j - N j=1 1 p j + 1 φ j 2 = 1 0 N j=1 φ j z p j 2 dz - 1 0 N j=1 φ j z p j dz 2 ≥ 0
by the Cauchy-Schwarz inequality. Moreover, the equality holds if and only if N j=1 φ j z p j is constant for z ∈ [0, 1], that is, φ = 0. This shows that A 0a 0 ⊗ a 0 is positive.

Next, we note that for any invertible matrix A and any vector x we have

det 0 x T x A = -(det A)x • A -1 x.
This equality comes easily from the identity

1 -x T A -1 0 Id 0 x T x A = -x • A -1 x 0 T x A .
Since A 1 is also positive, for each ξ ∈ R the matrix ξ 2 (A 0a 0 ⊗ a 0 ) + A 1 is positive too. Therefore, we have q(ξ 2 ) > 0, which yields the second assertion of the lemma. It is easy to see that q(ξ 2 ) is a polynomial in ξ 2 of degree less than or equal to N -1 and that the coefficient of ξ

2(N -1) is - 0 (1 -a 0 ) T 1 -a 0 A 0 -a 0 ⊗ a 0 ,
which is positive due to the positivity A 0a 0 ⊗ a 0 . Therefore, we obtain the first assertion of the lemma.

We denote the inverse matrix by

0 (1 -a 0 ) T 1 -a 0 (δξ) 2 (A 0 -1 ⊗ a 0 ) + A 1 -1 = q((δξ) 2 ) q((δξ) 2 ) T q((δξ) 2 ) Q((δξ) 2 ) ,
where q(ξ 2 ) = (q 1 (ξ 2 ), . . . , q N (ξ 2 )) T and Q(ξ 2 ) = (q ij (ξ 2 )) 1≤i,j≤N . Then, the solution (ϕ 0 , ϕ) to (5.4) can be expressed as (5.6) φ0 = q((δξ) 2 ) f0 + q((δξ) 2 ) • f , φ = q((δξ) 2 ) f0 + Q((δξ) 2 ) f .

We note that q(ξ 2 ), q i (ξ 2 ), and q ij (ξ 2 ) are rational functions in ξ 2 , more precisely, we can express them as

q(ξ 2 ) = q 1 ξ 2 + q 0 + p(ξ 2 ) q(ξ 2 ) , q i (ξ 2 ) = q 0i + p i (ξ 2 ) q(ξ 2 ) , q ij (ξ 2 ) = p ij (ξ 2 ) q(ξ 2 ) ,
for i, j = 1, . . . , N , where q(ξ 2 ) is the polynomial in ξ 2 of degree N -1 defined by (5.5). Moreover, p(ξ 2 ), p i (ξ 2 ), and p ij (ξ 2 ) are polynomials in ξ 2 of degree less than N -1. Therefore, by taking the inverse Fourier transform of (5.6) we obtain (5.7)

       ϕ 0 = q 1 δ 2 f ′′ 0 + q 0 f 0 + r δ * f 0 + N j=1 r jδ * f j , ϕ = q 0 f 0 + r δ * f 0 + R δ * f ,
where q 0 = (q 01 , . . . , q 0N ) T , r(x) = (r 1 (x), . . . , r N (x)) T , R(x) = r ij (x) 1≤i,j≤N , and r(x), r j (x), r ij (x) are Fourier inverse of p(ξ 2 ) q(ξ 2 ) ,

p j (ξ 2 ) q(ξ 2 ) , p ij (ξ 2 )
q(ξ 2 ) , respectively. We also used the notation

f δ (x) = δ -1 f (δ -1 x) for any function f (x).
In view of these solution formulae, we consider a function r(x) defined by

(5.8) r(x) = 1 2π R p(ξ 2 ) q(ξ 2 ) e ixξ dξ,
where q(ξ 2 ) and p(ξ 2 ) are polynomials in ξ 2 of degree N and of degree less than N -1, respectively, and q(ξ 2 ) ≥ c 0 > 0. It is easy to see that r(x) is a real valued, even, and continuous function on R. Since q(ξ 2 ) is a polynomials in ξ 2 of degree N -1 with real coefficients and positive definite, roots of q(ξ 2 ) = 0 have the form

ξ = α k ± iβ k , k = 1, 2, . . . , N -1 with 0 < β 1 ≤ β 2 ≤ • • • ≤ β N -1 .
Therefore, by the residue theorem we have an expression

r(x) = N -1 k=1 r ± k e iα k x-β k |x| for x ≷ 0
with some complex constants r ± 1 , . . . , r ± N -1 . By taking into account the continuity at x = 0, we have also

r ′ (x) = N -1 k=1 r ± k (iα k ∓ β k )e iα k x-β k |x| for x ≷ 0.
We note that the second derivative r ′′ (x) contains in general the Dirac delta function. Thanks of these expressions, we have the following lemma.

Lemma 5.3. Let r(x) be defined by (5.8). Then, r(x) is a real value even function and r ∈ W 1,∞ (R). Moreover, there exists positive constants β 1 and C such that for any x ∈ R we have a pointwise estimate

|r(x)| + |r ′ (x)| ≤ Ce -β 1 |x| .
For δ > 0, we put r δ (x) = δ -1 r(δ -1 x) and consider the function r δ * f . We remind the function spaces B k e and B k o for k = 0, 1, . . . defined in Section 1 and that the norm • was defined by (1.6).

Lemma 5.4. Let r(x) be defined by (5.8) and fix δ 0 such that 0 < δ 0 < β 1 . Then, there exists a constant C such that for any f ∈ B 0 α (α = e or o) and δ ∈ (0, δ 0 ] we have

r δ * f ∈ B 1 α . Moreover, it holds that r δ * f + δ (r δ * f ) ′ ≤ C f .
Proof. It follows from Lemma 5.3 that

|(r δ * f )(x)| ≤ 1 δ R r x -y δ |f (y)|dy ≤ C δ f R e -β 1 δ |x-y|-|y| dy = C f 1 β 1 + δ e -|x| + e -β 1 δ |x| + 1 β 1 -δ e -|x| -e -β 1 δ |x| ≤ 4C β 2 1 -δ 2 0 f e -|x| , which implies r δ * f ≤ 4C β 2 1 -δ 2 0
f . In view of (r δ * f ) ′ = r ′ δ * f , a similar estimate holds for (r δ * f ) ′ . Moreover, it is easy to see that if f is even or odd, then so is r δ * f , respectively. Therefore, we obtain the desired result.

In order to give an estimate for the solution (ϕ 0 , ϕ) to (5.4), it is convenient to introduce the following weighted norm (5.9)

u k+2,δ = u k + δ u k+1 + δ 2 u k+2
for k = 0, 1, 2, . . .. By the above arguments, we obtain the following proposition.

Proposition 5.5. There exist positive constants δ 0 and C such that for any f 0 , f ∈ B ∞ α (α = e or o) and any δ ∈ (0, δ 0 ], there exists a unique solution ϕ 0 , ϕ ∈ B ∞ α to (5.4). Moreover, for any k = 0, 1, 2, . . ., the solution satisfies

ϕ 0 k + ϕ k+2,δ ≤ C( f 0 k+2,δ + f k ), δ 2 ϕ ′′ k ≤ C(δ 2 f ′′ 0 k + f k ).

Existence of small amplitude solitary waves

We begin to give an existence theorem of the solution (ζ, ψ 0 , ψ) to the system of linear ordinary differential equations (4.9). Proposition 6.1. There exists a positive constant δ 0 such that for any

F 0 , F N +1 ∈ B ∞ e , any F ∈ B ∞
o , and any δ ∈ (0, δ 0 ], there exists a unique solution (ζ, ψ 0 , ψ) to (4.9

) satisfying ζ, ψ ′ 0 ∈ B ∞ e , ψ ∈ B ∞
o , and ψ 0 (0) = 0. Moreover, for any k = 0, 1, 2, . . ., the solution satisfies

ψ ′ 0 k+2 + ζ k+2,δ + ψ k+3,δ ≤ C 0 ( (F 0 , F N +1 ) k+2,δ + F k+1 ) + C k ( (F 0 , F N +1 ) 2,δ + F 1 ),
where C k is a positive constant depending on k while C 0 does not.

Proof. Thanks of Lemma 4.1, it is sufficient to solve (4.11)-(4.12) for (ψ 0 , ψ, χ) and then to define ζ by (4.10). To solve (4.11)-(4.12), we use the standard iteration argument by applying the existence theorems, that is, Propositions 5.1 and 5.5 given in the previous section. Suppose that ψ0 is given so that ψ′ 0 ∈ B ∞ e . By Proposition 5.5 under the condition 0 < δ ≤ δ 0 there exists a unique solution (ϕ

0 , ϕ) ∈ B ∞ e to (1 -a 0 ) • ϕ = F 0 + (2γ -η (0) )F N +1 + (3η (0) -4γ) ψ′ 0 , (1 -a 0 )ϕ 0 -δ 2 (A 0 -1 ⊗ a 0 )ϕ ′′ + A 1 ϕ = F ′ .
Then, we define χ and ψ by

χ(x) = x 0 ϕ 0 (y)dy, ψ(x) = x 0 ϕ(y)dy,
which are odd functions and satisfy

(6.1) (1 -a 0 ) • ψ ′ = F 0 + (2γ -η (0) )F N +1 + (3η (0) -4γ) ψ′ , ( 1
-a 0 )χ -δ 2 (A 0 -1 ⊗ a 0 )ψ ′′ + A 1 ψ = F .
Then, by Proposition 5.1 there exists a unique solution ψ 0 to (6.2)

-γψ ′′′ 0 + (4γ -3η (0) )ψ ′ 0 = F 0 + (2γ -η (0) )F N +1 + γ • F ′ -δ 2 β • ψ ′′′ satisfying ψ ′ 0 ∈ B ∞
e and ψ 0 (0) = 0. By using these solutions (χ, ψ, ψ 0 ), we define maps

T 0 : ψ0 → ψ 0 , T 1 : ψ0 → χ, T 2 : ψ0 → ψ. Clearly, T 0 maps X = {ψ 0 ∈ C ∞ (R) | ψ ′ 0 ∈ B ∞ e , ψ 0 (0) = 0}
into itself. We will show that T 0 is a contraction map with respect to an appropriate norm. To this end, let ψ0 ∈ X and let (χ, ψ, ψ 0 ) be the solutions as above. By Proposition 5.5 we have

χ ′ k + ψ ′ k+2,δ ≤ C( (F 0 , F N +1 ) k+2,δ + F k+1 + ψ′ 0 k+2 ) + C k ( F N +1 + ψ′ 0 ), (6.3) δ 2 ψ ′′′ k ≤ C (F 0 , F N +1 ) k+2,δ + F k+1 + δ 2 ψ′ 0 k+2 ) + C k ( F N +1 + δ 2 ψ′ 0 ). (6.4)
By Proposition 5.1 we have

ψ ′ 0 k+2 ≤ C( (F 0 , F N +1 ) k + F k + δ 2 ψ ′′′ k ) + C k ( (F 0 , F N +1 ) + F + δ 2 ψ ′′′ ),
which together with (6.4) implies

ψ ′ 0 k+2 ≤ C( (F 0 , F N +1 ) k+2,δ + F k+1 + δ 2 ψ′ 0 k+2 ) + C k ( (F 0 , F N +1 ) + F + δ 2 ψ′ 0 ).
Particularly, we obtain

ψ ′ 0 2 ≤ C( (F 0 , F N +1 ) 2,δ + F 1 + δ 2 ψ′ 0 2 ).
Therefore, by taking δ 0 so small that 2Cδ 2 0 ≤ 1, we obtain

ψ ′ 0 2 ≤ 1 2 ψ′ 0 2 + C( (F 0 , F N +1 ) 2,δ + F 1 )
and

ψ ′ 0 k+2 ≤ 1 2 ψ′ 0 k+2 + C( (F 0 , F N +1 ) k+2,δ + F k+1 ) (6.5) + C k ψ′ 0 2 + C k ( (F 0 , F N +1 ) 2,δ + F 1 ).
In exactly the same way as above, we obtain also

     T 0 ( ψ0 ) ′ -T 0 (ψ 0 ) ′ 2 ≤ 1 2 ψ ′ 0 -ψ′ 0 2 , T 0 ( ψ0 ) ′ -T 0 (ψ 0 ) ′ k+2 ≤ 1 2 ψ ′ 0 -ψ′ 0 k+2 + C k ψ ′ 0 -ψ′ 0 2 , T 1 ( ψ0 ) ′ -T 1 (ψ 0 ) ′ k + T 2 ( ψ0 ) ′ -T 2 (ψ 0 ) ′ k+2,δ ≤ C k ψ ′ 0 -ψ′ 0 k+2 .
On the other hand, it is easy to see that for any function u satisfying u(0) = 0 we have u L ∞ ≤ u ′ . Therefore, by the contraction mapping principle, the map T 0 has a unique fixed point ψ 0 ∈ X. Using this fixed point ψ 0 , we put χ = T 2 (ψ 0 ) and ψ = T 2 (ψ 0 ). Then, we see easily that (ψ 0 , χ, ψ) is a solution to (4.11)-(4.12). Moreover, it follows from (6.5) and (6.3) that

ψ ′ 0 k+2 + ψ ′ k+2,δ ≤ C ′ ( (F 0 , F N +1 ) k+2,δ + F k+1 ) + C ′ k ( (F 0 , F N +1 ) 2,δ + F 1 ),
where C ′ is a positive constant independent of k whereas the constant C ′ k depends on k. It follows from Lemma 4.1 that χ = ψ ′′ 0 so that

ψ = A -1 1 (F -(1 -a 0 )ψ ′′ 0 + δ 2 (A 0 -1 ⊗ a 0 )ψ ′′ ), which implies that ψ ≤ C( F + ψ ′ 0 2 + ψ ′ 2,δ
). We note that ψ k+3,δ ≤ ψ ′ k+2,δ +3 ψ . Therefore, by defining ζ by (4.10) we see that (ζ, ψ 0 , ψ) is the solution to (4.9) satisfying the desired estimate. Uniqueness of the solution can be shown as in the above calculation under the restriction 0 < δ ≤ δ 0 .

In order to prove one of our main result in this paper, that is, Theorem 1.1, it is sufficient to show an existence of the solution (ζ, ψ 0 , ψ) to (4.8) together with a uniform bound of the solution with respect to the small parameter δ. To this end, we need to give estimates of remainder terms (f 0 , f , f N +1 ) together with (g 0 , g, g N +1 ) in (4.8). It is not difficult to show the following lemma. Lemma 6.2. Suppose that F (u) is a polynomial of u such that F (0) = 0. Then, for any k = 2, 3, 4, . . . and any δ ∈ (0, 1] we have

F (u) k+2,δ ≤ C( u ) u k+2,δ + C(k, u k+1,δ ), F (u) k+1 ≤ C( u ) u k+1 + C(k, u ) u 1 u k + C(k, u k-1 ).
We note again that g 0 and g N +1 are polynomials in (η

(0) , η ′ (0) , η ′′ (0) ), that g is a polynomial in (η (0) , η ′ (0) , η ′′′ (0) ), and that g 0 , g N +1 ∈ B ∞ e and g ∈ B ∞ o . Moreover, f 0 and f N +1 are polynomials in (η (0) , η ′ (0) , η ′′ (0) , ζ, ψ ′ 0 , ψ, ψ ′ ), and f is a polynomial in (η (0) , η ′ (0) , η ′′′ (0) , ζ, ψ ′′ 0 , ψ, δ 2 ψ ′′ )
, whose coefficients are polynomials in δ. Therefore, applying Lemma 6.2 to (f 0 , f , f N +1 ) we obtain the following lemma.

Lemma 6.3. Suppose that ψ ′ , ζ ∈ B ∞ e , ψ ∈ B ∞ o , and δ ∈ (0, 1] satisfy ψ ′ 0 k+2 + ζ k+2,δ + ψ k+3,δ ≤ M k for k = 2, 3, 4, . . .. Then, it holds that f 0 , f N +1 ∈ B ∞ e , f ∈ B ∞ o ,
and that for k = 3, 4, 5, . . . we have

(f 0 , f N +1 ) 4,δ + δ f 3 ≤ C(M 2 ), (f 0 , f N +1 ) k+2,δ + δ f k+1 ≤ C(M 2 )M k + C(k, M k-1 ).
Now, we are ready to prove Theorem 1.1. We will construct the solution (ζ, ψ 0 , ψ) to (4.8) by the standard iteration arguments. To this end, we introduce a function space

X = {(ζ, ψ 0 , ψ) ∈ C ∞ (R) | ζ, ψ ′ 0 ∈ B ∞ e , ψ ∈ B ∞ 0 , ψ 0 (0) = 0, |||(ζ, ψ 0 , ψ)||| k,δ ≤ M k for k = 1, 2, 3, . . .}, where |||(ζ, ψ 0 , ψ)||| k,δ = ψ ′ 0 k+2 + ζ k+2,δ + ψ k+3,δ
and the constants M k for k = 1, 2, 3, . . . will be defined later. Suppose that ( ζ, ψ0 , ψ) ∈ X. Then, by Lemma 6.3 and Proposition 6.1, under the condition 0 < δ ≤ δ 0 there exists a unique solution (ζ, ψ 0 , ψ) to (6.6)

     (η (0) -2γ)ζ + 2(γ -η (0) )ψ ′ 0 + (1 -a 0 ) • ψ ′ = g 0 + δ 2 f0 , (1 -a 0 )ψ ′′ 0 -δ 2 (A 0 -1 ⊗ a 0 )ψ ′′ + A 1 ψ = g + δ 2 f , ζ + ψ ′ 0 = g N +1 + δ 2 fN+1 satisfying ζ, ψ ′ 0 ∈ B ∞ e , ψ ∈ B ∞ 0
, and ψ 0 (0) = 0, where f0 , f , fN+1 are given by f 0 , f , f N +1 with (ζ, ψ 0 , ψ) replaced by ( ζ, ψ0 , ψ). Moreover, the solution satisfies

|||(ζ, ψ 0 , ψ)||| 2,δ ≤ C + δC(M 2 ), |||(ζ, ψ 0 , ψ)||| k,δ ≤ C(k, M k-1 ) + δC(M 2 )M k
for k = 3, 4, 5, . . .. In view of these estimates, we put M 2 = 2C and define M k inductively by M k = 2C(k, M k-1 ) for k = 3, 4, 5, . . .. Then, by taking δ 0 so small that 2δ 0 C(M 2 ) ≤ C and 2δ 0 C(M 2 ) ≤ 1 we see that (ζ, ψ 0 , ψ) ∈ X. Therefore, if we define a map T : ( ζ, ψ0 , ψ) → (ζ, ψ 0 , ψ), then T maps X into itself. Moreover, in exactly the same way as above, we obtain

     |||T ( ζ, ψ0 , ψ) -T (ζ, ψ 0 , ψ)||| 2,δ ≤ 1 2 |||( ζ, ψ0 , ψ) -(ζ, ψ 0 , ψ)||| 2,δ , |||T ( ζ, ψ0 , ψ) -T (ζ, ψ 0 , ψ)||| k,δ ≤ 1 2 |||( ζ, ψ0 , ψ) -(ζ, ψ 0 , ψ)||| k,δ + C(k, M k )|||( ζ, ψ0 , ψ) -(ζ, ψ 0 , ψ)||| k-1
,δ for k = 3, 4, 5, . . .. Therefore, by the contraction mapping principle, the map T has a unique fixed point (ζ, ψ 0 , ψ) ∈ X, which is a solution to (4.8) and satisfies

ψ ′ 0 k+2 + ζ k+2,δ + ψ k+3,δ ≤ M k for k = 2, 3, 4, . . .
with a constant M k independent of δ ∈ (0, δ 0 ]. The proof of Theorem 1.1 is complete.

7 Numerical analysis for large amplitude solitary waves

In the previous section, we proved the existence of small amplitude solitary wave solutions to the Isobe-Kakinuma model (1.3). In the present section, we will analyze numerically large amplitude solitary wave solutions to the model in the special case where the parameters are chosen as N = 1 and p 1 = 2. Even in this special case, the Isobe-Kakinuma model gives a better approximation than the Green-Naghdi equations in the shallow water and strongly nonlinear regime. Therefore, we will consider the equations (7.1)

           cη + Hφ ′ 0 + 1 3 H 3 φ ′ 1 = 0, φ ′′ 0 + 1 5 H 2 φ ′′ 1 + 2δ -2 φ 1 = 0, c(φ ′ 0 + H 2 φ ′ 1 ) + η + 1 2 (φ ′ 0 + H 2 φ ′ 1 ) 2 + 2δ -2 H 2 φ 2 1 = 0
under the boundary conditions at the spatial infinity (7.2) η(x), φ ′ 0 (x), φ ′ 1 (x), φ 1 (x) → 0 as x → ±∞ and the symmetry

(7.3) η(-x) = η(x), φ 0 (-x) = -φ 0 (x), φ 1 (-x) = -φ 1 (x),
where H = 1 + η. In this case, the constant γ in Theorem 1.1 is given by γ = 1 3 so that we can put (7.4)

c = 1 + 2 3 δ 2
and regard δ as a bifurcation parameter. Moreover, it follows from Proposition 2.2 that solutions to (7.1)-( 7.2) satisfy

(7.5) η 2 -H(φ ′ 0 ) 2 - 2 3 H 3 φ ′ 0 φ ′ 1 - 1 5 H 5 (φ ′ 1 ) 2 + 4 3 δ -2 H 3 φ 2 1 = 0.
For numerical analysis, it is convenient to rewrite the equations in (7.1) as a system of ordinary differential equations of order 1. To this end, we introduce a new unknown function

(7.6) u = φ ′ 0 + H 2 φ ′ 1 ,
which is the horizontal component of the velocity on the water surface. Observe that the first equation in (7.1) and (7.6) can be rewritten into a system

H 1 3 H 3 1 H 2 φ ′ 0 φ ′ 1 = -cη u ,
or equivalently

(7.7) φ ′ 0 φ ′ 1 = 1 2 3 H 3 -H 2 (cη + 1 3 Hu) cη + Hu .
Differentiating the first equation in (7.1) and (7.6), we obtain

H 1 3 H 3 1 H 2 φ ′′ 0 φ ′′ 1 = -(c + u)η ′ u ′ -2Hφ ′ 1 η ′ , or equivalently φ ′′ 0 φ ′′ 1 = 1 2 3 H 3 -(c + u)H 2 + 2 3 H 4 φ ′ 1 η ′ -1 3 H 3 u ′ (c + u) -2H 2 φ ′ 1 η ′ + Hu ′ .
Plugging these into the second equation in (7.1) yields

(7.8) -6(c + u)H + 2H 3 φ ′ 1 η ′ -H 2 u ′ + 10δ -2 H 2 φ 1 = 0.
On the other hand, we can rewrite the third equation in (7.1) as

cu + η + 1 2 u 2 + 2δ -2 H 2 φ 2 1 = 0.
Differentiating this yields (7.9)

(c + u)u ′ + (1 + 4δ -2 Hφ 2 1 )η ′ + 4δ -2 H 2 φ 1 φ ′ 1 = 0.
Now, it follows from (7.7)-(7.9) that (7.10)

                 η ′ = 6H(cη + Hu) + 10H 2 (c + u) δ 2 {6H(c + u) 2 -3(c + u)(cη + Hu) -H 2 (1 + 4Hφ 2 1 )} φ 1 , u ′ = - 18(cη + Hu) 2H(c + u) -(cη + Hu) + 10H 3 (1 + 4Hφ 2 1 ) δ 2 H{6H(c + u) 2 -3(c + u)(cη + Hu) -H 2 (1 + 4Hφ 2 1 )} φ 1 , φ ′ 1 = 3 2H 3 (cη + Hu).
To summarize, (7.1)-( 7.3) has been transformed equivalently into (7.10) under the boundary conditions at the spatial infinity (7.11) η(x), u(x), φ 1 (x) → 0 as x → ±∞ and the symmetry (7.12) η(-x) = η(x), u(-x) = u(x), φ 1 (-x) = -φ 1 (x).

Proposition 7.1. Any regular solution (η, u, φ 1 ) to (7.10)-(7.11) satisfies the two identities

(7.13)      cu + η + 1 2 u 2 + 2δ -2 H 2 φ 2 1 = 0, η 2 -Hu 2 + 2u(cη + Hu) - 6 5H (cη + Hu) 2 + 4 3 δ -2 H 3 φ 2 1 = 0.
Proof. The first identity is nothing but the third equation in (7.1). Plugging (7.7) into (7.5), we obtain the second one.

In order to obtain numerical solutions to (7.10)-(7.12), it is sufficient to determine the initial data (η(0), u(0), φ 1 (0)). It follows from (7.12) that φ 1 (0) = 0, which together with the identities in (7.13) implies (7.14)

     cu(0) + η(0) + 1 2 u(0) 2 = 0, η(0) 2 -H(0)u(0) 2 + 2u(0) cη(0) + H(0)u(0) - 6 5H(0) cη(0) + H(0)u(0) 2 = 0,
where H(0) = 1 + η(0) and c is given by (7.4). Particularly, by eliminating η(0) from these two identities we obtain (7.15) 7u(0) 4 + 42cu(0

) 3 + 6(13c 2 -3)u(0) 2 + 8c(13c 2 -8)u(0) + 8(6c 2 -1)(c 2 -1) = 0.
This is a quartic equation in u(0) so that for each given c we have four roots. Generally, two of them are complex numbers and one real root does not give the correct initial data for the solitary wave solution, so that we can determine the initial data (η(0), u(0), φ 1 (0)) for appropriately chosen δ. We proceed to compare solitary wave solutions to the Isobe-Kakinuma model (7.1)-(7.4) calculated numerically as above with the classical solitons of the Korteweg-de Vries equation (7.16) η KdV (x) = 4 3 δ 2 sech 2 x, which is the first approximation for small amplitude solitary wave solutions to the Isobe-Kakinuma model as was guaranteed by Theorem 1.1. In Figure 7.1, we plot the surface profile η(x) of the solitary wave solutions to the Isobe-Kakinuma model (7.1) and the soliton η KdV (x) of the Korteweg-de Vries equation given by (7.16) for several values of δ. We observe that for small δ the error ηη KdV L ∞ is small as expected. As δ increases, the error cannot be negligible anymore and the wave height of the solitary wave to the Isobe-Kakinuma model becomes larger than that of the classical soliton. We can catch numerically the solitary wave solutions to the Isobe-Kakinuma model for δ up to some critical value δ c . For δ beyond this critical value δ c , the quartic equation (7.15) does not have any real root so that the solitary wave solution might not exist. This suggests that there exists a maximum height of the solitary wave solutions to the Isobe-Kakinuma model as in the case of the full water wave problem. In Figures 7.2 and 7.3, we plot also the surface profiles of the solitary wave solutions to the Isobe-Kakinuma model for several values of δ in the same figures. We observe that the wave height is monotonically increasing as δ increases and that a sharp crest is formed as δ approaches the critical value δ c . We will analyze more precisely this formation of a sharp crest. To this end, we calculate numerically the curvature κ at the crest of the surface profile, which is defined by

(a) (b) (c) (d) (e) (f)
κ(x) = η ′′ (x) 1 + (η ′ (x)) 2 3 2
.

We also introduce a function d(x) by (7.17)

d = 6H(c + u) 2 -3(c + u)(cη + Hu) -H 2 (1 + 4Hφ 2 1 )
, where H = 1 + η and c is given by (7.4). This function appears in the denominator of the right-hand side of the ordinary differential equations for η and u in (7.10). In the solitary wave solutions to the Isobe-Kakinuma model for several values of δ. We observe that as δ approaches some critical value δ c , the wave height converges toward a maximum wave height η c (0), the curvature at the crest is blowing up, and the denominator at the crest is going to vanish. This consideration suggests strongly the existence of solitary wave of extreme form as well as a sharp crest to the Isobe-Kakinuma model and that the critical value δ c would be obtained by the equation d(0) = 0, that is, (7.18) 6H(0) c + u(0) 2 -3 c + u(0) cη(0) + H(0)u(0) -H(0) 2 = 0, where H(0) = 1 + η(0) and c is given by (7.4). In fact, we can calculate this critical value δ c , the maximum wave height η c (0), the horizontal velocity u c (0) of the water at the crest, and the critical phase speed c c by solving nonlinear algebraic equations (7.15) and (7.18) together with (7.4). Those values are approximately given by (7.19) δ c = 0.62633493, η c (0) = 0.687926, u c (0) = -0.797196, c c = 1.26153.

In Figures 7.4 and 7.5, we plot the surface and horizontal velocity profiles of the solitary wave of extreme form to the Isobe-Kakinuma model. It follows from (7.19) that c c + u c (0) > 0, which means that the crest of the solitary wave of extreme form is not the stagnation point unlike the full water wave problem. We proceed to calculate the angle of the crest of the solitary wave of extreme form. To this end, it is sufficient to evaluate η ′ c (±0), where (η c , u c , φ 1c ) is the solution to the Isobe-Kakinuma model (7.10) in the critical case δ = δ c . We denote by d c the corresponding denominator defined by (7.17) so that by the first equation in (7.10) we have Here, note that we have rewritten all physical quantities in a nondimensional form. In order to calculate the angle of the crest in the physical space, we have to work with dimensional variables. Let x * and η * be the horizontal spatial coordinate and the surface elevation in the physical space, respectively, so that we have x * = λx and η * = hη, where h is the mean depth of the water and λ the typical wavelength. The angle of the crest in the physical space should be calculated from η * Now, the included angle θ of the shape crest in the physical space is approximately given by θ = 152.6 • , which is larger than the included angle 120 • of the sharp crest of the solitary wave solution of extreme form to the full water wave problem.

  Φ(x, z, t)) 2 + (∂ z Φ(x, z, t)) 2 + gz dz,

Figure 1 Figure 1 . 1 :

 111 Figure 1.1: Solitary wave of extreme form with the included angle θ = 152.6 • .

Lemma 4 . 1 .

 41 If ζ, ψ 0 , ψ, and χ solve (4.10)-(4.12) and satisfies χ(0) = ψ ′′ 0 (0), then we have χ = ψ ′′ 0 . Particularly, ζ, ψ 0 , and ψ solve (4.9).

Figure 7 . 1 :

 71 Figure 7.1: Surface profiles of the solitary wave solutions to the Isobe-Kakinuma model (solid line) and the Korteweg-de Vries equation (dashed line) for several values of δ: (a) δ = 0.3, (b) δ = 0.45, (c) δ = 0.55, (d) δ = 0.6, (e) δ = 0.62, (f) δ = 0.62633493.

  whereH c = 1 + η c and v c = c c + u c .It follows from the third equation in (7.10) that (7.21) φ ′ 1c (

Figure 7 . 4 : 2 Figure 7 . 5 :

 74275 Figure 7.4: Surface profile of the solitary wave of extreme form to the Isobe-Kakinuma model.

c′

  (±0). In view of the relation η* (x * ) = hη(λ -1 x * ), we have η * ′ (x * ) = δη ′ (x) so that η * c ′ (±0) = δ c η ′ c (±0), that is, η * c ′ (±0) = ∓ 3v c (0) H c (0)v c (0)c c 8H c (0)v c (0) -3c c H c (0) 2 3v c (0) 3 -8H c (0)v c (0) -3c c = 0.24397.

Table 7 .

 7 1, we list the wave height, the curvature at the crest, and the value of the denominator d at the crest of

						0.70
		0.8
						0.68
		0.6				0.66
						0.64
		0.4				0.62
						0.60
		0.2				0.58
						0.56
						-0.10	-0.05	0.00	0.05	0.10
	-4	-2	0	2	4
	Figure 7.2: Surface profiles of the solitary wave solutions to the Isobe-Kakinuma model for δ = 0.45, 0.55, 0.6, 0.62, 0.62633493.	Figure 7.3: Surface profiles near the crests of the solitary wave solutions to the Isobe-Kakinuma model for δ = 0.6, 0.62, 0.625, 0.626, 0.62633493.

  Table 7.1: List of the wave height, the curvature at the crest, and the value of the denominator d at the crest of the solitary wave solutions to the Isobe-Kakinuma model.

	.6	0.581258	2.34087	1.55722
	0.62	0.645485	4.85676	7.30167×10 -1
	0.625	0.670918	1.04536×10	3.23799×10 -1
	0.626 0.6263 0.62633	0.679938 0.685463 0.687014	2.0651 ×10 6.3354 ×10 1.68098×10 2	1.59473×10 -1 5.08746×10 -2 1.90423×10 -2
	0.626334 0.6263349 0.62633493	0.687532 0.687855 0.687915	3.8648 ×10 2 2.12563×10 3 1.384 ×10 4	8.26255×10 -3 1.5 ×10 -3 2.30314×10 -4

2H c (0) 3 H c (0)v c (0)c c .