# An Encoding for CLP Problems in SMT-LIB

Daneshvar Amrollahi University of Tehran<EMAIL_ADDRESS>TeIAS, Khatam
University
University of Tehran University of Regensburg
Uppsala University Hossein Hojjat TeIAS, Khatam University
University of Tehran<EMAIL_ADDRESS>University of Regensburg
Uppsala University Philipp Rümmer University of Regensburg
Uppsala University<EMAIL_ADDRESS>
###### Abstract

The input language for today’s CHC solvers are commonly the standard SMT-LIB
format, borrowed from SMT solvers, and the Prolog format that stems from
Constraint-Logic Programming (CLP). This paper presents a new front-end of the
Eldarica CHC solver that allows inputs in the Prolog language. We give a
formal translation of a subset of Prolog into the SMT-LIB commands. Our
initial experiments show the effectiveness of the approach and the potential
benefits to both the CHC solving and CLP communities.

##  1 Introduction

Over the last years, a growing number of solvers for Constrained Horn Clauses
(CHC) have been developed; for instance, Spacer [9], Eldarica [6], Golem [2],
and RInGEN [3]. There are two main languages used to interface such solvers:
the SMT-LIB language [4], in which Horn clauses can either be expressed using
quantified assertions, or using the rule-based notation that was introduced by
Z3; and dialects of Prolog [7] as a language in Constraint-Logic Programming
(CLP). The former language is designed primarily for machine-generated input
to solvers, as it is simple to parse, strongly typed, and has unambiguous
semantics. The latter language is more concise and convenient for handwritten
programs. There is, unfortunately, no exact match between the theories
considered in CLP and SMT-LIB, and some Prolog language features have
semantics that are not straightforward to model; for instance, the default
absence of the “occurs-check” in equations.

This paper presents an ongoing effort to add a comprehensive Prolog/CLP front-
end to the CHC solver Eldarica [6]. Eldarica has been able to process clauses
in Prolog format since the beginning of its development; however, the existing
Prolog front-end of Eldarica is restricted to the parsing of clauses over
integers, and it is planned to replace it with a front-end with more extensive
support for the different Prolog features through this project. To document
the applied interpretation of Prolog, we define a formal translation of a
fragment of Prolog to the SMT-LIB language. In the scope of this paper, we
focus on three key features of Prolog: functions, defining a Herbrand universe
of values; lists; and integer numbers as introduced by CLP($\mathbb{Z}$). We
model the semantics of those language features using a mapping to SMT-LIB
data-types (i.e., algebraic data-types with free constructors) and SMT-LIB
integers.

#### Example

To illustrate the complementarity of CHC and CLP, we start with a simple
routing example including integer arithmetic, lists, and functions in Prolog.
Figure 1 shows a CLP($\mathbb{Z}$) program to compute the distance between
cities. The program consists of 9 facts and 2 rules. A fact of the form
distance($X$, $Y$, $Z$) states that the direct distance between cities $X$ and
$Y$ is $Z$. The rule in line 12 implies that distance is symmetric. The
meaning of path($X$, $Y$, $Z$, $L$) is that there exists a path of length $Z$
from $X$ to $Y$ where $L$ represents the path as a list of points in the
format waypoint($C$, $D$). This shows that city $C$ lies on the path from $X$
to $Y$ with a distance of $D$ from the starting point, which is $X$. The fact
path(A, A, 0, [waypoint(A, 0)]). states that for any city A, there is a path
of length 0 to itself and the list presenting the path is the city A itself.
Finally, the rule on line 15 implies that if there is path N of length P from
A to B, and the direct distance from B to C is Q and D is equal to P + Q, then
we have found a path from A to C, which is the previously found path (N)
extended with the city C. The query path(tehran, munich, D, X), D #< 40.
searches for a path from munich to tehran of length less than 40. A possible
answer to this query is D = 34 and X = [waypoint(munich,34),
waypoint(vienna,31), waypoint(tehran,0)]. This means that there is a path from
tehran to munich of distance 34, with vienna being on the way with distance 31
from tehran.

Note that this Prolog program, while intuitive, is also rather inefficient,
and interpreting it using a CLP engine might lead to non-termination due the
recursion on lines 12,15. The program can be rewritten to a more operationally
oriented (and harder to read) set of clauses to be terminating and efficient,
in particular preventing cyclic paths from being explored, and inlining the
length bound to allow branches without solutions to be pruned. Alternatively,
tabling [5] could be used for the predicate path111Which, however, led to an
error in experiments with SWI-Prolog [12]..

CHC solvers are generally less efficient than Prolog engines for solving
constraint satisfaction problems. However, the abstraction techniques in CHC
solvers are naturally able to cope with clauses written in declarative and
otherwise inefficient style. They can easily find a path from tehran to munich
of length 40 in Figure 1. CHC solvers are also able to determine that no such
path exists for lengths less than 34, a task more challenging for at least
some CLP solvers. More generally, CHC solvers are agnostic of the order of
clauses, and the order of literals in clauses, and process clauses focusing
more on their logical content than syntactic features. In this sense, CHC
solvers can be a useful debugging tool, and have a complementary performance
profile to CLP systems. The goal of our work is to simplify the integration of
CLP and CHC methods, by providing a translation of a subset of Prolog into
SMT-LIB, the common input language of CHC solvers.

⬇

1:- use_module(library(clpz)). % or clpfd

2

3distance(tehran, vienna, 31).

4distance(vienna, paris, 10).

5distance(vienna, munich, 3).

6distance(paris, munich, 10).

7distance(paris, rome, 11).

8distance(lausanne, rome, 6).

9distance(lausanne, munich, 4).

10distance(tehran, paris, 42).

11

12distance(A, B, D) :- distance(B, A, D).

13

14path(A, A, 0, [waypoint(A, 0)]).

15path(A, C, D, [waypoint(C, D) | N]) :- path(A, B, P, N), distance(B, C, Q),

16 D #= P + Q.

17

18?- path(tehran, munich, D, X), D #< 40.

Figure 1: Prolog Program for distance between cities in CLP($\mathbb{Z}$)

_Organization of the paper:_ In Section 2 we overview the CLP and the SMT-LIB
input languages. Section 3 discusses translation rules for converting Prolog
to SMT-LIB. Section 4 translates the introductory example to SMT-LIB. We
conclude the paper and present directions of future research in Section 5.

##  2 Preliminaries

###  2.1 Constraint Logic Programming (CLP)

Constraint Logic Programming (CLP) [11], first introduced by Jaffar and Lassez
in 1987 [8], is a programming paradigm that combines the benefits of
constraint programming and logic programming. It enables the modeling of
complicated real-world problems with variables and constraints, and uses
logical and constraint reasoning to find a solution. CLP expresses the
connections between variables as constraints and looks for a derivation of
queries from given clauses.

Prolog is the main language of CLP, where the constraints are equations over
the algebra of terms. CLP problems may in addition contain symbols with pre-
defined meanings, defined by a _theory_. CLP($\mathbb{Z}$) [10] refers to CLP
over the theory of integer arithmetic. Figure 2 is a simplified grammar that
is able to parse Prolog programs with functions, lists, and integer
arithmetic. An extended version of it is used in our actual implementation.

¡Database¿ ::= ¡Clause¿∗

¡Clause¿ ::= ¡Predicate¿ ‘.’ ¡Predicate¿ ‘:-’ ¡BodyItem¿∗ ‘.’ ‘?-’ ¡BodyItem¿∗
‘.’

¡BodyItem¿ ::= ¡Predicate¿ ¡Constraint¿

¡Predicate¿ ::= ¡Atom¿ ¡Atom¿ ‘(’ ¡Term¿∗ ‘)’

¡Term¿ ::= ¡Variable¿ ¡Atom¿ ¡Atom¿ ‘(’ ¡Term¿∗ ‘)’ ¡List¿ ¡Integer¿

¡List¿ ::= ‘[’ ¡Term¿∗ ‘]’ ‘[’ ¡Term¿∗ ‘—’ ¡Term¿ ‘]’

Figure 2: A simplified grammar for describing the syntax of Prolog programs.

As shown in Figure 2, every Prolog program consists of a set of _Clause_ s. A
clause has a _head_ and a _body_. The head can have zero or one predicates,
and the body is a list of predicates and constraints. A clause is either a
_Fact_ , a _Rule_ , or a _Query_. For example, man(tom) is a fact, and
friends(X, Y) :- likes(X, Y), likes(Y, X) is a rule with friends(X, Y) as the
head and likes(X, Y), likes(Y, X) as the body. Queries always start with a ?-.
For instance, ?- likes(X, tom) would search for an assignment for X such that
likes(X, tom) can be derived from the set of given clauses. _Term_ s can be
variables, atoms, compound terms, lists, and integers.

Structured data is represented using compound terms. A compound term consists
of a function and a sequence of one or more sub-terms. A function is
characterized by its name, which is an atom, and its arity. For instance, in
the fact man(father(claire)), the term father(claire) is a compound term.

In Prolog, there are different kinds of built-in equality operators (#=, =,
=:=, is) with different semantics. The =/2 predicate, which accepts two
arguments, is used to ensure that its two arguments are syntactically equal
through unification. For instance, the response to the query ?- father(X) =
father(john) will be positive as the sub-terms can be unified by setting X =
john. By default, Prolog does not apply any “occurs-check”, however, which can
sometimes cause non-termination. An example of this is ?- X = father(X). The
unification algorithm decides to unify X with the right-hand-side, which is
father(X). But still there is an X left in this term; interpretation can get
stuck in this loop of replacing X by father(X) and never terminate.

_List_ s are terms representing sequences of elements; for instance, [a, [b,
c], 7] is a list of terms. A non-empty list can be also be thought of as
having two parts: _head_ as the first element of the list, and _tail_ as the
remainder of the list. Both representations can be parsed using the grammar
rules in Figure 2.

The body of the clauses in a Prolog program may also include _constraint_ s,
in addition to predicates. An example of a constraint in CLP($\mathbb{Z}$),
Constraint Logic Programming over the domain of integers, is X + Y #>= 3 * Z -
17. Some other operators for constraints in CLP($\mathbb{Z}$) include #=, #>,
#>=, #<, #=<, +, -, *, /, mod. Throughout the rest of this paper, whenever we
refer to constraints, we refer to constraints in CLP($\mathbb{Z}$).

###  2.2 SMT-LIB

SMT-LIB, or the Satisfiability Modulo Theories Library [4], is a standardized
format for specifying logical formulas modulo various background theories. It
is widely used in applications like software verification, hardware design,
and automated reasoning, and is also used as a standard input format of CHC
solvers. The SMT-LIB language supports a range of theories, including
arithmetic, bit-vectors, and arrays, allowing users to express a wide variety
of constraints.

An SMT-LIB script consists of a list of commands to be processed by an SMT
solver. Important SMT-LIB commands are:

  * •

(set-logic $L$): Set the logic, i.e., the combination of theories that will be
used. For CHC solvers, typically $L=\texttt{HORN}$.

  * •

(declare-fun $f$ ($T_{1}~{}\ldots~{}T_{n}$) $T$): Declaration of a function or
predicate $f$ with the given argument types $T_{1}~{}\ldots~{}T_{n}$ and
result type $T$. Types in SMT-LIB include the types provided by background
theories (e.g., Int for integers, Bool for Booleans), as well as user-defined
types. When interfacing CHC solvers, typically only predicates (i.e., Boolean-
valued functions) are declared.

  * •

(declare-datatype $T$ ($C_{1}~{}\ldots~{}C_{n}$)): Declaration of an algebraic
data-type $T$ with constructors $C_{1}~{}\ldots~{}C_{n}$. Data-types can be
recursive, and are the main modelling technique in SMT-LIB to represent
structured data. For every constructor $C$, the data-type declaration will
also introduce a tester (_ is $C$) to identify terms constructed using $C$, as
well as selectors for the arguments. An extended version of the command,
declare-datatypes, exists to define several mutually recursive data-types. We
will see various examples of algebraic data-types in this article.

  * •

(assert $\phi$): Assert a constraint $\phi$, which can be formulated using the
standard operators of first-order logic, the functions and predicates provided
by background theories, and declared symbols. CHC solvers require that
asserted constraints $\phi$ are _constrained Horn clauses,_ which means that
they fall into one of the following classes of formulas:

Facts: | ($p$ $t_{1}~{}\ldots~{}t_{k}$)
---|---
Quantified facts: | (forall ($X_{1}~{}\ldots~{}X_{n}$) ($p$ $t_{1}~{}\ldots~{}t_{k}$))
Rules: | (forall ($X_{1}~{}\ldots~{}X_{n}$) (=> (and $\psi_{1}~{}\ldots~{}\psi_{m}$) ($p$ $t_{1}~{}\ldots~{}t_{k}$)))
Queries: | (forall ($X_{1}~{}\ldots~{}X_{n}$) (=> (and $\psi_{1}~{}\ldots~{}\psi_{m}$) false)

  * •

(check-sat): Instruct the SMT solver to check whether the constraints asserted
up to this point are satisfiable.

Throughout the paper, only a small subset of the SMT-LIB commands are used.
For a full definition of SMT-LIB, we refer to the standard documentation [4].

##  3 Translating CLP to SMT-LIB

In this section, we explain our translation from CLP problems in Prolog to
SMT-LIB. We begin by a motivating example as a warm-up. After that, we present
the translation rules for Prolog facts, rules, lists, and CLP($\mathbb{Z}$)
constraints. We remark that our implementation does not explicitly translate
input problems to SMT-LIB, but instead directly constructs clauses using
Eldarica’s internal data structures; the translation to SMT-LIB is presented
for documentation purposes, and reflects the semantics that is applied.

⬇

(declare-datatype U (

(claire)

(father (father_1 U))

)

)

⬇

(declare-fun man

(U)

Bool

)

⬇

(assert

(man (father claire))

)

Figure 3: SMT-LIB equivalent of man(father(claire))

###  3.1 A Motivating Example

Consider the Prolog fact man(father(claire)). This fact consists of the
function father applied to an atomic term claire. To model this term, one
could consider declaring corresponding uninterpreted functions in SMT-LIB.
However, with uninterpreted functions, claire and father(claire) might be
assigned the same value, despite being syntactically different terms: the
equation (= claire (father claire)) is satisfiable in SMT-LIB. This is
inconsistent with Prolog semantics, in which claire and father(claire) are
different and non-unifiable terms, and it is guaranteed that they stand for
distinct elements of the Herbrand universe. In addition, most CHC solvers do
not support uninterpreted functions.

We therefore propose to treat claire and father as constructors of an
algebraic data-type. To translate the mentioned fact to SMT-LIB, the first
step is to introduce a new algebraic data-type for all of the terms occurring
in a program. The data-type will be called U, standing for _U_ niversal. The
constructors of U will be all atoms and functions appearing in the clauses.
Figure 3 shows the full translation of the example. The constructor father is
unary, and its definition also adds a selector father_1 to retrieve the sub-
term. We also define the predicate man, as a Boolean function with a single
argument of type U. Finally, we add the fact man(father(claire)) to the set of
our clauses using the assert command. Section 3.2 provides further details.

It has to be noted that our encoding of terms does not exactly model Prolog
semantics. As explained in Section 2, the unification algorithm of Prolog will
not detect the non-unifiability of a query ?- X = father(X) due to the missing
occurs-check. In contrast, elements of SMT-LIB data-types are finite
constructor terms, which implies that the equation (= X (father X)) is not
satisfiable in SMT-LIB. However, we believe that the finite-term semantics is
usually the intended semantics of a Prolog program. It remains to be
investigated in future work whether there is a way to represent Prolog
semantics more closely in SMT-LIB.

$\mathit{collectFunctions}(t)=\begin{cases}\\{(atom,0)\\},&\text{if
}t=\mathit{atom}\\\
\\{(c,n)\\}\cup\bigcup_{i=1}^{i=n}\mathit{collectFunctions}(a_{i}),&\text{if
}t=c(a_{1},\cdots,a_{n})\\\ \emptyset,&\text{otherwise}\\\ \end{cases}$ Figure
4: Function $\mathit{collectFunctions}$ collecting functions in the terms

⬇

(declare-datatype U

(

($f_{1}$ ($f_{1}^{1}$ U) ... ($f_{1}^{a_{1}}$ U))

...

($f_{n}$ ($f_{n}^{1}$ U) ... ($f_{n}^{a_{n}}$ U))

)

Figure 5: Definition of the universal type U for functions
$\\{(f_{1},a_{1}),\ldots,(f_{n},a_{n})\\}$

###  3.2 Algebraic Data Types (ADTs)

We define a single algebraic data-type U for representing the type of all
terms in a program. The constructors of U will be all functions and atoms
appearing in the clauses. As this global type U is defined only once, we need
to iterate through all clauses and collect the functions and atoms appearing
in them. We define a recursive function responsible for this matter in Figure
4. This function is applied to a term $t$, and recursively collects the atoms
and functions occurring in $t$, as well as their arity. For instance, the
value of $\mathit{collectFunctions}(a(X,b,c(d,Y,e)))$ is
$\\{(e,0),(d,0),(c,3),(b,0),(a,3)\\}$.

Given that the set collected using $\mathit{collectFunctions}$ is
$\\{(f_{1},a_{1}),\ldots,(f_{n},a_{n})\\}$, the universal algebraic data type
U should be defined as in Figure 5.

$\begin{array}[]{c@{\qquad}c}\inference{}{a\;\triangleright\;a\;:\emptyset}[aisanatom]&\inference{}{V\;\triangleright\;V\;:\emptyset}[Visavariable]\\\\[21.52771pt]
\lx@intercol\hfil\inference{\\{t_{i}\;\triangleright\;t_{i}^{\prime}\;:\;\Phi_{i}\\}_{i=1}^{n}}{\texttt{f($t_{1}$,...,$t_{n}$)}\;\triangleright\;\texttt{(f
$t_{1}^{\prime}$ ...
<EMAIL_ADDRESS>\inference{s\;\triangleright\;s^{\prime}\;:\;\Phi_{1}\quad t\;\triangleright
t^{\prime}\;:\;\Phi_{2}}{\texttt{$s$ = $t$}\;\triangleright\;\texttt{(=
$s$${}^{\prime}$
$t$${}^{\prime}$)}\;:\;\Phi_{1}\cup\Phi_{2}}[]&\inference{s\;\triangleright\;s^{\prime}\;:\;\Phi}{\texttt{
\textbackslash+$s$}\;\triangleright\;\texttt{(not
$s$${}^{\prime}$)}\;:\;\Phi}[]\\\\[21.52771pt]
\lx@intercol\hfil\inference{s\;\triangleright\;s^{\prime}\;:\;\Phi_{1}\quad
t\;\triangleright\;t^{\prime}\;:\;\Phi_{2}}{\texttt{$s$ =\textbackslash=
$t$}\;\triangleright\;\texttt{(not (= $s$${}^{\prime}$
$t$${}^{\prime}$))}\;:\;\Phi_{1}\cup\Phi_{2}}[]\hfil\lx@intercol\end{array}$
Figure 6: Basic rules for translating Prolog to SMT-LIB

⬇

(declare-fun $p$

(U ... U)

Bool

)

⬇

(assert

(forall ( ($X_{1}$ U) ... ($X_{m}$ U) )

(=> (and $\Phi_{1}$ ... $\Phi_{n}$) ($p$ $t_{1}^{\prime}$ ...
$t_{n}^{\prime}$))

)

)

Figure 7: Translation of a fact $p(t_{1},\ldots,t_{n})$. We assume that the
elements of a set $\Phi_{i}$ are implicitly conjoined.

###  3.3 Translation of Facts

Section 3.1 shows an example of translating a fact to SMT-LIB. We now
introduce the general case of this translation, and add rules for lists and
integer arithmetic in Sections 3.5 and 3.6. We refer to triplets of the form
$\texttt{s}\;\triangleright\;\texttt{s}^{\prime}\;:\;\Phi$ as _translation
judgement_ s. The meaning of a judgement is that the Prolog term s can be
translated to an SMT-LIB term s′ under a set of side conditions $\Phi$. Side
conditions are mainly needed to capture typing requirements. For instance,
Prolog (CLP($\mathbb{Z}$)) raises an error when encountering the expression a
+ b, where a or b are not integers. Thus, when translating a + b to SMT-LIB,
we will later add side conditions that ensure the correct type of a and b.
More details concerning the use of side conditions are given in Sections 3.5
and 3.6.

Figure 6 shows the basic translation rules. Each rule derives a translation
judgement, the conclusion under the bar, from premises shown above the bar.
The rules in Figure 6 are mostly self-explanatory, and recursively translate a
given term or constraint to SMT-LIB. The rules assume, for sake of
presentation, that atoms, variables, and functions are translated to SMT-LIB
symbols with the same name.

The SMT-LIB translation of a Prolog fact $p(t_{1},\ldots,t_{n})$ is shown in
Figure 7 in terms of expressions $t_{1}^{\prime},\ldots,t_{n}^{\prime}$ and
side conditions $\Phi_{1},\ldots,\Phi_{n}$, which are defined as follows:

  * •

For all $i\in\\{1,\ldots,n\\}$ it holds that
$t_{i}\;\triangleright\;t_{i}^{\prime}\;:\;\Phi_{i}$.

  * •

$X_{1},\ldots,X_{m}$ are all the variables appearing in the terms
$t_{1},\ldots,t_{n}$.

The fact is captured using an SMT-LIB assertion in Figure 7, listing the side
conditions required by the translation as assumptions.

⬇

(declare-fun likes

(U U)

Bool

)

(declare-fun friends

(U U)

Bool

)

⬇

(assert

(forall ( (X U) (Y U) )

(=>

(and (likes X Y) (likes Y X))

(friends X Y)

)

)

)

Figure 8: Translation of a rule in SMT-LIB

⬇

(assert

(forall ( ($X_{1}$ U) ... ($X_{k}$ U) )

(=> (and $\psi_{1}^{\prime}\;\ldots\;\psi_{m}^{\prime}$ $\Phi_{0}$ ...
$\Phi_{m}$) $\psi^{\prime}_{0}$)

)

)

Figure 9: Translation of a rule
$\psi_{0}\;\texttt{:-}\;\psi_{1},\ldots,\psi_{m}$

###  3.4 Translation of Rules

Before presenting the translation of rules, we begin with a concrete
example, using the Prolog rule friends(X, Y) :- likes(X, Y), likes(Y, X). This
rule will be turned into a universally quantified implication in SMT-LIB.
Given that we have already defined our universal data-type U as explained in
Section 3.2, all we need is to declare functions in SMT-LIB for likes and
friends, and create the rule using the universal quantifier. The full
translation is illustrated in Figure 8.

The general schema for expressing a rule
$\psi_{0}\;\texttt{:-}\;\psi_{1},\ldots,\psi_{m}$ in SMT-LIB is shown in
Figure 9, assuming that:

  * •

For all $i\in\\{0,\ldots,m\\}$ it holds that
$\psi_{i}\;\triangleright\;\psi_{i}^{\prime}\;:\;\Phi_{i}$.

  * •

$X_{1},\ldots,X_{k}$ are all the variables appearing in the rule.

The assertion representing the rule in Figure 9 has a similar shape as the
assertion for facts in Figure 7.

⬇

(declare-datatypes () (

(U

(aList (theList L))

...

)

(L

nil

(cons (head U) (tail L))

)

)

)

Figure 10: Algebraic data-types including lists

⬇

list_concat([],L,L).

list_concat([X1|L1],L2,[X1|L3]) :- list_concat(L1,L2,L3).

Figure 11: A Prolog program concatenating lists

⬇

(declare-fun list_concat (U U U) Bool)

(assert (forall ((X U)) (list_concat (aList nil) X X)))

(assert (forall ((X1 U) (L1 U) (L2 U) (L3 U))

(=> (and (list_concat L1 L2 L3) ((_ is aList) L1) ((_ is aList) L3))

(list_concat

(aList (cons X1 (theList L1))) L2 (aList (cons X1 (theList L3))))))

)

Figure 12: SMT-LIB representation of the program in Figure 11
$\displaystyle\inference{}{\texttt{[]}\;\triangleright\;\texttt{(aList
nil)}\;:\emptyset}[]$
$\displaystyle\inference{\\{t_{i}\;\triangleright\;t_{i}^{\prime}\;:\;\Phi_{i}\\}_{i=1}^{n}}{\texttt{
[$t_{1}$,...,$t_{n}$] }\triangleright\texttt{ (aList (cons $t_{1}^{\prime}$
(cons $t_{2}^{\prime}$ (... cons $t_{n}^{\prime}$
nil))...))}\triangleright\;\bigcup_{i=1}^{n}\Phi_{i}}[]$
$\displaystyle\inference{h\;\triangleright\;h^{\prime}\;\triangleright\;\Phi_{1}\quad
t\;\triangleright\;t^{\prime}\;\triangleright\;\Phi_{2}}{\texttt{[$h$|$t$]}\;\triangleright\;\texttt{
(aList (cons $h^{\prime}$ (theList $t^{\prime}$)))
}\;:\;\Phi_{1}\cup\Phi_{2}\cup\\{\texttt{((\\_ is aList) $t^{\prime}$)}\\}}[]$
Figure 13: Translation rules for lists

###  3.5 Translation of Lists

We now add lists to the picture. The absence of static typing in Prolog makes
it a-priori impossible to tell whether a Prolog variable will represent a list
or a term constructed using some function (or possibly both). We therefore
include lists as one case in our universal data-type U, and ensure the correct
typing of terms through side-conditions in our translation rules.

Lists can be viewed as an algebraic data-type (call it L) with two
constructors nil and cons. The constructor nil has zero arguments and
represents empty lists, and cons has two arguments: one referring to the head
of the list (a term of type U), and one of type L referring to the tail of the
list.

To implement lists in SMT-LIB, it is therefore natural to declare a new data-
type L with the nil and cons constructors. This new data-type will have a
mutual dependency on our universal data-type U, as defined before, and
therefore has to be declared along with U as shown Figure 10. Note that in
Figure 10, there may be other constructors for U coming from the collected
functions in Section 3.2, denoted by three dots. The aList constructor is
introduced to wrap terms of type L as a term of the universal type U. An
example of a Prolog program involving lists is presented in Figure 11. The
translation of the program in Figure 11 to SMT-LIB is presented in Figure 12.

A set of inference rules for translating lists in Prolog to SMT-LIB is
presented in Figure 13. The first rule in Figure 13 translates the empty list.
The second rule represents the translation of a list with explicitly
enumerated elements. In this case, the list can be constructed in SMT-LIB as a
simple iterated application of cons. The final rule directly matches the
functional definition of a list. A list in Prolog with $h$ as the head, and
$t$ as the tail, can be constructed using the cons constructor in SMT-LIB.
This construction is type-correct only if $t$ is again a list; thus, the rule
adds the side condition ((_ is aList) $t^{\prime}$), and unwraps the tail
using the theList selector. In all the rules in Figure 13, the result is
finally wrapped using the aList constructor and turned into a U-term.

⬇

(declare-datatypes () (

(U

(anInt (theInt Int))

...

)

)

)

Figure 14: Modified declaration of the universal ADT for integer arithmetic
$\displaystyle\inference{s\;\triangleright\;s^{\prime}\;:\;\Phi_{1}\quad
t\;\triangleright\;t^{\prime}\;:\;\Phi_{2}}{s\star
t\;\triangleright\;\texttt{(anInt ($\mathit{op}$ (theInt $s^{\prime}$) (theInt
$t^{\prime}$)))}\;:\;\Phi_{1}\cup\Phi_{2}\cup\\{\texttt{(\\_ is anInt)
$s^{\prime}$)},\texttt{(\\_ is anInt) $t^{\prime}$)}\\}}[]$
$\displaystyle\text{where~{}~{}}(\star,\mathit{op})\in\\{\texttt{(+,+),
(-,-),(*,*),(/,div),(mod,mod)}\\}$
$\displaystyle\inference{s\;\triangleright\;s^{\prime}\;:\;\Phi_{1}\quad
t\;\triangleright\;t^{\prime}\;:\;\Phi_{2}}{s\circ
t\;\triangleright\;\texttt{($\mathit{op}$ (theInt $s^{\prime}$) (theInt
$t^{\prime}$))}\;:\;\Phi_{1}\cup\Phi_{2}\cup\\{\texttt{(\\_ is anInt)
$s^{\prime}$)},\texttt{(\\_ is anInt) $t^{\prime}$)}\\}}[]$
$\displaystyle\text{where~{}~{}}(\circ,\mathit{op})\in\\{\texttt{(\\#=,=),
(\\#>,>),(\\#>=,>=),(\\#<,<),(\\#=<,<=)}\\}$
$\displaystyle\inference{}{I\;\triangleright\;\texttt{(anInt
$I$)}\;:\;\emptyset}[Iisadecimalnon-negativeinteger]$
$\displaystyle\inference{}{\texttt{-}I\;\triangleright\;\texttt{(anInt (-
$I$))}\;:\;\emptyset}[Iisadecimalnon-negativeinteger]$ Figure 15: Translation
rules for expressions and contraints in CLP($\mathbb{Z}$)

###  3.6 Integer Arithmetic

We finally introduce inference rules for converting constraints in the
background theory of integer arithmetic (e.g., 2*X + 7 #> Y) to their
corresponding expressions in SMT-LIB. To represent integers, similarly as with
lists we add a new constructor to U, so that we can wrap integers into a term
of type U. We call this new constructor anInt, and define it in Figure 14. We
once again note that U is a universal type and may include other constructors.

The translation rules for integer expressions and Boolean constraints over
them are presented in Figure 15. The first rule translates integer-valued
functions by recursively translating the sub-terms, unwrapping the result, and
applying the corresponding SMT-LIB function. The result is finally wrapped
again using anInt. The second rule performs the corresponding translation for
integer predicates. The other two rules take care of the translation of
integer literals.

The translation can be modified easily to model bounded integers, which are
used by some Prolog implementations. In this case, instead of Int in Figure
14, a bit-vector type like (_ BitVec 64) has to be used, and in Figure 15 the
corresponding bit-vector operations have to be applied. Bit-vector support in
CHC solvers is much less mature than support for mathematical integers,
however.

As an example, consider the expression X #> 7. According to the translation
rule for variables in Figure 6, $\texttt{X}\;\triangleright\;X\;:\;\emptyset$,
and according to the translation rule for integers in Figure 15,
$\texttt{7}\;\triangleright\;\texttt{(anInt 7)}\;:\;\emptyset$. Finally,
according to the first rule in Figure 15 for translating expressions in
integer arithmetic, the whole expression gets translated to (anInt (+ (theInt
X) (theInt (anInt 7)))), with the side constraint that X is an integer.

##  4 An SMT-LIB Encoding of the Motivating Example

Combining the different Prolog features that were discussed, Figure 16 gives
the SMT-LIB encoding of the Prolog program for computing paths between cities
from Section 1. All the commands used in this encoding can be obtained using
the translation rules explained throughout this article. The encoding begins
by declaring the universal data-type U. Its constructors include all the atoms
and functions that appear in the clauses, in addition to anInt and aList.
After that, the data-type L is declared for lists, as explained in Section
3.5. The SMT-LIB script continues by declaring the functions distance and path
appearing in the Prolog program clauses. The rest of the encoding are
assertions corresponding to the Prolog rules and facts, and finally the
assertion as a clause with head false.

A CHC solver like Eldarica [6] can derive the status unsat for this SMT-LIB
script, which implies that the clauses are contradictory. This can be
interpreted as the negation of the last clause being derivable from the other
clauses. A CHC solver could also discover the path discussed in Section 1.

When tightening the length bound to (< (theInt D) 34), the problem becomes
satisfiable, which can again be verified using a CHC solver.

⬇

1(declare-datatypes () (

2 (U

3 (anInt (theInt Int))

4 (aList (theList L))

5 (waypoint (waypoint_1 U) (waypoint_2 U))

6 tehran vienna paris munich rome lausanne

7 )

8 (L

9 nil

10 (cons (head U) (tail L))

11 )

12 )

13)

14(declare-fun distance (U U U) Bool)

15(declare-fun path (U U U U) Bool)

16

17(assert (distance tehran vienna (anInt 31)))

18(assert (distance vienna paris (anInt 10)))

19(assert (distance vienna munich (anInt 3)))

20(assert (distance paris munich (anInt 10)))

21(assert (distance paris rome (anInt 11)))

22(assert (distance lausanne rome (anInt 6)))

23(assert (distance lausanne munich (anInt 4)))

24(assert (distance tehran paris (anInt 42)))

25(assert

26 (forall ( (A U) (B U) (D U) )

27 (=> (distance B A D) (distance A B D))

28 )

29)

30(assert

31 (forall ( (A U) )

32 (path A A (anInt 0) (aList (cons (waypoint A (anInt 0)) nil)))

33 )

34)

35(assert

36 (forall ( (A U) (B U) (C U) (D U) (N U) (P U) (Q U) )

37 (=>

38 (and

39 (path A B P N) (distance B C Q)

40 (= D (anInt (+ (theInt P) (theInt Q))))

41 ((_ is aList) N) ((_ is anInt) P) ((_ is anInt) Q)

42 )

43 (path A C D (aList (cons (waypoint C D) (theList N))))

44 )

45 )

46)

47(assert

48 (forall ( (D U) (X U) )

49 (=>

50 (and (path tehran munich D X) (< (theInt D) 40) ((_ is anInt) D))

51 false

52 )

53 )

54)

55

56(check-sat)

Figure 16: The SMT-LIB encoding of the motivating example introduced in the
introduction

##  5 Conclusion

We have presented work towards a new CHC solver front-end that allows input in
Prolog format, bridging the gap between Prolog/CLP semantics and SMT-LIB. We
are in the process of implementing the defined translation from Prolog to SMT-
LIB in our Horn solver Eldarica [6], with the goal of achieving good coverage
of the Prolog and CLP features.

The translation defined in this paper should be seen as a starting point, as
there are several aspects that require further work, more research, or more
discussion in the communities:

  * •

We have only shown the translation rules for some of the most important
CLP($\mathbb{Z}$) operators. We believe that many other theories and
constraints can be handled in a similar fashion.

  * •

We keep typing constraints dynamic, and this way stay close to the actual
Prolog semantics. In terms of the efficiency of CHC solvers on the translated
program, of course, it could be beneficial to perform some amount of type
inference upfront. This way, one could translate integer variables in Prolog
to native SMT-LIB Int variables, etc. However, CHC solvers with support for
algebraic data-types tend to perform such type inference themselves, so that
the payoff from being more clever during the translation is unclear.

  * •

Our translation includes all typing constraints as assumptions (Figures 7 and
9), i.e., the well-typedness of a Prolog program is assumed but not verified.
It is not entirely obvious how correct typing should be asserted in the SMT-
LIB representation, however. In the list example in Figure 11, for instance,
note that the first clause implies that the second and third argument of
list_concat can be terms of any kind, whereas the second clause relies on the
third argument being a list. The clauses therefore entail ill-typed statements
like list_concat([X|[]], 42, [X|42]]). A CLP engine performing backward
chaining will, however, not run into any typing errors.

  * •

There are several aspects of Prolog semantics that are challenging in a
translation to SMT-LIB. Those include, in particular, the _missing occurs-
check_ in equations, as well as _cuts._ It is unclear whether those features
can or should be translated faithfully to SMT-LIB semantics.

Finally, it will be interesting to evaluate solver performance for the
different design choices in the translation, for different CHC solvers, and to
compare to the performance of state-of-the-art CLP engines. We have not done
such a comparison yet due to the preliminary state of the implementation of
the front-end. While we generally assume CLP to be significantly more
efficient on classical constraint satisfaction problems than CHC, there might
also be areas in which the abstraction-based algorithms used in CHC solvers
have advantages.

## References

  * [1]
  * [2] _The Golem Horn Solver_.  Available at https://github.com/usi-verification-and-security/golem.
  * [3] _RInGen: Regular Invariant Generator_.  Available at https://github.com/Columpio/RInGen.
  * [4] Clark Barrett, Pascal Fontaine & Cesare Tinelli (2017): _The SMT-LIB Standard: Version 2.6_.  Technical Report, Department of Computer Science, The University of Iowa.  Available at www.SMT-LIB.org.
  * [5] W. Chen & D. S. Warren (1996): _Tabled Evaluation with Delaying for General Logic Programs_.  Journal of the ACM 43(1), pp. 20–74, 10.1016/0304-3975(89)90088-1.
  * [6] Hossein Hojjat & Philipp Rümmer (2018): _The ELDARICA Horn Solver_.  In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1–7, 10.23919/FMCAD.2018.8603013.
  * [7] ISO (1995): _ISO/IEC 13211-1:1995: Information technology — Programming languages — Prolog — Part 1: General core_.  Available at http://webstore.ansi.org/ansidocstore/product.asp?sku=ISO%2FIEC+13211%2D1%3A1995;http://www.iso.ch/cate/d21413.html.
  * [8] J. Jaffar & J.-L. Lassez (1987): _Constraint Logic Programming_.  In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’87, Association for Computing Machinery, New York, NY, USA, p. 111–119, 10.1145/41625.41635.
  * [9] Anvesh Komuravelli, Arie Gurfinkel & Sagar Chaki (2014): _SMT-Based Model Checking for Recursive Programs_.  In Armin Biere & Roderick Bloem, editors: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Lecture Notes in Computer Science 8559, Springer, pp. 17–34, 10.1007/978-3-319-08867-9_2.
  * [10] Markus Triska (2012): _The Finite Domain Constraint Solver of SWI-Prolog_.  In Tom Schrijvers & Peter Thiemann, editors: Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings, Lecture Notes in Computer Science 7294, Springer, pp. 307–316, 10.1007/978-3-642-29822-6_24.
  * [11] Mark Wallace (2002): _Constraint Logic Programming_ , pp. 512–532.  Springer Berlin Heidelberg, Berlin, Heidelberg, 10.1007/3-540-45628-7_19.
  * [12] Jan Wielemaker, Tom Schrijvers, Markus Triska & Torbjörn Lager (2010): _SWI-Prolog_.  arXiv:https://arxiv.org/abs/1011.5332.


Dedicated to Professor Tohru Ozawa on the occasion of his sixties birthday

# Recent developments on the lifespan estimate for classical solutions of
nonlinear wave equations
in one space dimension

Hiroyuki Takamura  Mathematical Institute, Tohoku University, Aoba, Sendai
980-8578, Japan<EMAIL_ADDRESS>
###### Abstract.

In this paper, we overview the recent progresses on the lifespan estimates of
classical solutions of the initial value problems for nonlinear wave equations
in one space dimension. There are mainly two directions of the developments on
the model equations which ensure the optimality of the general theory. One is
on the so-called “combined effect” of two kinds of the different nonlinear
terms, which shows the possibility to improve the general theory. Another is
on the extension to the non-autonomous nonlinear terms which includes the
application to nonlinear damped wave equations with the time-dependent
critical case.

###### Key words and phrases:

nonlinear wave equation, initial value problem, one space dimension, classical
solution, lifespan

###### 2010 Mathematics Subject Classification:

primary 35L71, secondary 35B44

##  1\. Introduction.

In order to illustrate our purpose, let us turn back to the general theory for
nonlinear wave equations in one space dimension which was introduced by Li, Yu
and Zhou [18, 19] more than 30 years ago.

We consider the initial value problem of the form;

$\left\\{\begin{array}[]{ll}\displaystyle
u_{tt}-u_{xx}=H(u,u_{t},u_{x},u_{xx},u_{xt})&\quad\mbox{in}\ {\bf
R}\times(0,T),\\\ u(x,0)={\varepsilon}f(x),\quad
u_{t}(x,0)={\varepsilon}g(x)&\quad\mbox{for}\ x\in{\bf R},\end{array}\right.$
(1)

where $T>0$, $f,g\in C_{0}^{\infty}({\bf R})$ and ${\varepsilon}>0$ is a
sufficiantly small parameter. Let $\widetilde{\lambda}=(\lambda;\
(\lambda_{i}),i=0,1;\ (\lambda_{ij}),i,j,=0,1,i+j\geq 1).$ Assume that
$H=H(\widetilde{\lambda})$ is a sufficiently smooth function with

$H(\widetilde{\lambda})=O(|\widetilde{\lambda}|^{1+\alpha})$

in a neighborhood of $\widetilde{\lambda}=0$, where $\alpha\in{\bf N}$. Let us
define the lifespan $\widetilde{T}({\varepsilon})$ as the maximal existence
time of the classical solution of (1) with arbitrary fixed data. We are
interested in the long-time stability of the trivial solution due to the fact
that we cannot expect any time-decay of the solution of the free wave equation
in one space dimension. Indeed, the general theory is to express the lower
bound of $\widetilde{T}({\varepsilon})$ by means of the smallness of the
initial data, i.e. ${\varepsilon}$, for which, Li, Yu and Zhou [18, 19]
obtained

$\widetilde{T}({\varepsilon})\geq\left\\{\begin{array}[]{lll}C{\varepsilon}^{-\alpha/2}&\mbox{in
general case,}\\\ C{\varepsilon}^{-\alpha(1+\alpha)/(2+\alpha)}&\mbox{if}\
\displaystyle\int_{{\bf R}}g(x)dx=0,\\\
C{\varepsilon}^{-\min\\{\beta_{0}/2,\alpha\\}}&\mbox{if}\
\partial_{u}^{\beta}H(0)=0\ \mbox{for}\
1+\alpha\leq\forall\beta\leq\beta_{0},\end{array}\right.$ (2)

where $C$ is a positive constant independent of ${\varepsilon}$. This result
has been expected complete more than 30 years.

Beyond the general theory, our interest went to its optimality or to extending
the general theory by studying the morel problem;

$\left\\{\begin{array}[]{ll}\displaystyle
u_{tt}-u_{xx}=A(x,t)|u_{t}|^{p}|u|^{q}+B(x,t)|u|^{r}&\mbox{in}\quad{\bf
R}\times(0,T),\\\ u(x,0)={\varepsilon}f(x),\
u_{t}(x,0)={\varepsilon}g(x),&x\in{\bf R},\end{array}\right.$ (3)

where $p,q,r>1$ ($q$ could be zero) and $A,B$ are non-negative functions of
space-time variables. Let us write the lifespan of classical solutions of (3)
by $T({\varepsilon})$. According to the series of our studies on the estimates
of $T({\varepsilon})$, we will see later that the general theory can be
improved in some case, which arises from the constant coefficient case. This
part is presented in Section 2. Moreover, the principle in extending the
nonlinear term $H$ in (1) of the general theory to the non-autonomous one
$H=H(x,t,u,u_{t},u_{x},u_{xx},u_{xt})$ must be initiated by variable
coefficient case. This part is presented in Section 3.

##  2\. Case of constant coefficients and the combined effect.

In this section, we assume that

$A(x,t)\equiv A_{0}\quad\mbox{and}\quad B(x,t)\equiv B_{0}.$

where $A_{0}$ and $B_{0}$ are non-negative constants.

###  2.1. The generalized combined effect.

When $A_{0}=0$ and $B_{0}>0$, Zhou [36] obtained the estimates of
$T({\varepsilon})$;

$T({\varepsilon})\sim\left\\{\begin{array}[]{lll}C{\varepsilon}^{-(r-1)/2}&\mbox{if}&\displaystyle\int_{{\bf
R}}g(x)dx\neq 0,\\\
C{\varepsilon}^{-r(r-1)/(r+1)}&\mbox{if}&\displaystyle\int_{{\bf
R}}g(x)dx=0.\end{array}\right.$ (4)

Here we denote the fact that there are positive constants, $C_{1}$ and
$C_{2}$, independent of ${\varepsilon}$ satisfying $E({\varepsilon},C_{1})\leq
T({\varepsilon})\leq E({\varepsilon},C_{2})$ by $T({\varepsilon})\sim
E({\varepsilon},C)$. The classification by total integral of the initial speed
$g$ is caused by strong Huygens’ principle such as (17). On the other hand,
when $A_{0}>0$ and $B_{0}=0$, we have

$T({\varepsilon})\sim C{\varepsilon}^{-(p+q-1)}$ (5)

For $q=0$, the upper bound in this estimate was obtained by Zhou [37], and the
lower bound is due to Kitamura, Morisawa and Takamura [14]. For $q>1$, (5) was
verified by Zhou [38] for the upper bound with integer $p,q$ satisfying $p\geq
1,q\geq 0,p+q\geq 2$, and by Li,Yu and Zhou [18, 19] for the lower bound with
integer $p,q$ satisfying $p+q\geq 2$ including more general but smooth terms.
Note that [38] is a preprint version of Zhou [37] in which only the case of
$q=0$ is considered. But it is easy to apply its argument to the case of
$q>1$. The lower bound in this case is due to Kido, Sasaki, Takamatsu and
Takamura [11].

Therefore the natural expectation is that

$T({\varepsilon})\sim\left\\{\begin{array}[]{ll}C{\varepsilon}^{-\min\\{(p+q-1),(r-1)/2\\}}&\mbox{if}\
\displaystyle\int_{{\bf R}}g(x)dx\not=0\\\
C{\varepsilon}^{-\min\\{(p+q-1),r(r-1)/(r+1)\\}}&\mbox{if}\
\displaystyle\int_{{\bf R}}g(x)dx=0\end{array}\right.$ (6)

in the case where $A_{0}>0$ and $B_{0}>0$. But, surprisingly, we have the
following fact.

######  Theorem 1 (Morisawa, Sasaki and Takamura [23, 24], Kido, Sasaki,
Takamatsu and Takamura [11]).

The conjecture (6) is true except for the case where

$\int_{{\bf R}}g(x)dx=0\quad\mbox{and}\quad\frac{r+1}{2}<p+q<r.$ (7)

In this case, we have that

$T({\varepsilon})\sim C{\varepsilon}^{-(p+q)(r-1)/(r+1)},$ (8)

which is strictly shorter than the second case in (6).

The brief proof of (8) will appear at the end of this section. We shall call
this special phenomenon by “generalized combined effect” of two
nonlinearities. The original “combined effect”, which means the case of $q=0$,
was first observed by Han and Zhou [4] which targeted to show the optimality
of the result by Katayama [9] on the lower bound of the lifespan of classical
solutions of nonlinear wave equations with a nonlinear term $u_{t}^{3}+u^{4}$
in two space dimensions including more general nonlinear terms. It is known
that $T({\varepsilon})\sim\exp\left(C{\varepsilon}^{-2}\right)$ for the
nonlinear term $u_{t}^{3}$ and $T({\varepsilon})=\infty$ for the nonlinear
term $u^{4}$, but Katayama [9] obtained only a much worse estimate than their
minimum as $T({\varepsilon})\geq c{\varepsilon}^{-18}$. Surprisingly, more
than ten years later, Han and Zhou [4] showed that this result is optimal as
$T({\varepsilon})\leq C{\varepsilon}^{-18}$. They also considered (3) with
$q=0$ for all space dimensions $n$ bigger than 1 and obtain the upper bound of
the lifespan. Its counter part, the lower bound of the lifespan, was obtained
by Hidano, Wang and Yokoyama [5] for $n=2,3$. See the introduction of [5] for
the precise results and references. We note that the estimate (8) with $q=0$
coincides with the lifespan estimate for the combined effect in [4, 5] if one
sets $n=1$ formally. Indeed, [4] and [5] showed that

$T({\varepsilon})\sim C{\varepsilon}^{-2p(r-1)/\\{2(r+1)-(n-1)p(r-1)\\}}$ (9)

holds for $n=2,3$ provided

$(r-1)\\{(n-1)p-2\\}<4,\ 2\leq p\leq r\leq 2p-1,\ r>\frac{2}{n-1}.$ (10)

Later, Dai, Fang and Wang [3] improved the lower bound of lifespan for the
critical case in [5]. They also show that $T({\varepsilon})<\infty$ for all
$p,r>1$ in case of $n=1$, i.e. (3) with $q=0$. For the non-Euclidean setting
of the results above, see Liu and Wang [20] for example, in which the
application to semilinear damped wave equations is included.

###  2.2. Comparison with the general theory.

Here we strongly remark that our estimate in (8) is better than that of the
general theory by Li, Yu and Zhou [18, 19] in the case of (7) with integer
$p,q,r\geq 2$. Because our result on the lower bound of the lifespan can be
established also for the smooth terms as $u_{tt}-u_{xx}=u_{t}^{p}u^{q}+u^{r}$.
We note that there are infinitely many examples of $(p,q,r)=(m,m,2m+1)$ as the
inequality

$\frac{r+1}{2}=m+1<p+q=2m<r=2m+1$

holds for $m=2,3,4,\ldots$. This fact shows a possibility to improve the
general theory. We also note that, even for the original combined effect of
$q=0$, the integer points satisfying (10) are $(p,r)=(2,3),(3,3),(3,4)$ for
$n=2$ and $(p,r)=(2,2)$ for $n=3$, but (9) with $p=r$ agrees with the case of
$A_{0}=0$ and $B_{0}>0$. See Introduction of Imai, Kato, Takamura and Wakasa
[6] for references on the case of $A_{0}=0$ and $B_{0}>0$. Hence one can say
that only the lifespan estimates with $(p,r)=(2,3),(3,4)$ for $n=2$ are
essentially in the combined effect case. If $q\neq 0$, $p$ is replaced with
$p+q$ in the results above. Therefore it has less meaningful to consider (3)
in higher space dimensions, $n\geq 2$, if we discuss the optimality of the
general theory. In spite of this situation, Han and Zhou [4] studied

$u_{tt}-\Delta u=u|u_{t}|^{p-1}+u|u|^{q-1}\quad\mbox{in}\ {\bf
R}^{2}\times(0,T)$

with $1<p\leq 4,q>1$ to show the blow-up part of the generalized combined
effect.

Of course, some special structure of the nonlinear terms such as “null
condition” guarantees the global-in-time existence. See Nakamura [22], Luli,
Yang and Yu [21], Zha [34, 35] for examples in this direction. But we are
interested in the optimality of the general theory.

From now on, let us make sure the fact above. If one applies the result of the
general theory (2) to our problem (3) with

$H(u,u_{t},u_{x},u_{xx},u_{xt})=u_{t}^{p}u^{q}+u^{r}\quad\mbox{with}\
p,q,r\in{\bf N},$ (11)

one has the following estimates in each cases.

  * •

When $p+q<r$,

then, we have to set $\alpha=p+q-1$ and $\beta_{0}=r-1$ which yield that

$\widetilde{T}({\varepsilon})\geq\left\\{\begin{array}[]{ll}C{\varepsilon}^{-(p+q-1)/2}&\mbox{in
general},\\\ C{\varepsilon}^{-(p+q)(p+q-1)/(p+q+1)}&\mbox{if}\
\displaystyle\int_{{\bf R}}g(x)dx=0,\\\
C{\varepsilon}^{-\min\\{(r-1)/2,p+q-1\\}}&\begin{array}[]{l}\mbox{if
$\partial_{u}^{\beta}H(0)=0$}\\\ \mbox{for $p+q\leq\forall\beta\leq
r-1$}.\end{array}\end{array}\right.$

We note that the third case is available for (11). Therefore, for
$p+q\leq(r+1)/2$, we obtain that

$\widetilde{T}({\varepsilon})\geq c{\varepsilon}^{-(p+q-1)}$

whatever the value of $\displaystyle\int_{{\bf R}}g(x)dx$ is. On the other
hand, for $(r+1)/2<p+q$, i.e.

$\frac{r-1}{2}<p+q-1,$

we obtain

$\widetilde{T}({\varepsilon})\geq\left\\{\begin{array}[]{ll}C{\varepsilon}^{-(r-1)/2}&\mbox{if}\
\displaystyle\int_{{\bf R}}g(x)dx\neq 0,\\\
C{\varepsilon}^{-\max\\{(r-1)/2,(p+q)(p+q-1)/(p+q+1)\\}}&\mbox{if}\
\displaystyle\int_{{\bf R}}g(x)dx=0.\\\ \end{array}\right.$

  * •

When $p+q\geq r$,

then, similarly to the case above, we have to set $\alpha=r-1$, which yields
that

$\widetilde{T}({\varepsilon})\geq\left\\{\begin{array}[]{ll}C{\varepsilon}^{-(r-1)/2}&\mbox{in
general},\\\ C{\varepsilon}^{-r(r-1)/(r+1)}&\mbox{if}\ \displaystyle\int_{{\bf
R}}g(x)dx=0,\\\ C{\varepsilon}^{-\min\\{\beta_{0}/2,(r-1)\\}}&\mbox{if
$\partial_{u}^{\beta}H(0)=0$ for
$r\leq\forall\beta\leq\beta_{0}$}.\end{array}\right.$

We note that the third case does not hold for (11) by
$\partial_{u}^{r}H(0)\neq 0$.

As a conclusion, for the special nonlinear term in (11), the result of the
general theory is

$\widetilde{T}({\varepsilon})\geq\left\\{\begin{array}[]{ll}C{\varepsilon}^{-(p+q-1)}&\mbox{for}\
p+q\leq\displaystyle\frac{r+1}{2},\\\ C{\varepsilon}^{-(r-1)/2}&\mbox{for}\
\displaystyle\frac{r+1}{2}\leq p+q\end{array}\right.\mbox{if}\ \int_{{\bf
R}}g(x)dx\not=0\\\ $

and

$\widetilde{T}({\varepsilon})\geq\left\\{\begin{array}[]{l}C{\varepsilon}^{-(p+q-1)}\\\
\qquad\displaystyle\mbox{for}\ p+q\leq\displaystyle\frac{r+1}{2},\\\
C{\varepsilon}^{-\max\\{(r-1)/2,(p+q)(p+q-1)/(p+q+1)\\}}\\\
\qquad\displaystyle\mbox{for}\ \displaystyle\frac{r+1}{2}\leq p+q\leq r,\\\
C{\varepsilon}^{-r(r-1)/(r+1)}\\\ \qquad\mbox{for}\ r\leq p+q\\\
\end{array}\right.\mbox{if}\ \displaystyle\int_{{\bf R}}g(x)dx=0.$

Therefore a part of our results in (8) is larger than the lower bound of
$\widetilde{T}({\varepsilon})$ in that case. If one follows the proof of
Theorem 1, one can find that it is easy to see that our results on the lower
bounds also hold for a special term (11) by estimating the difference of
nonlinear terms from above after employing the mean value theorem. This fact
indicates that we still have a possibility to improve the general theory in
the sense that the optimal results in (8) should be included at least.

###  2.3. An improvement of the general theory.

Inspired by Theorem 1, Takamatsu [29] has recently proved the following
theorem which is an improvement of the general theory related to the
generalized combined effect.

######  Theorem 2 (Takamatsu [29]).

The third case,

$\partial_{u}^{\beta}H(0,0,0)=0\quad\mbox{for}\
\alpha+1\leq\forall\beta\leq\beta_{0},$

in the result of the general theory (2) is improved as

$\widetilde{T}({\varepsilon})\geq\left\\{\begin{array}[]{ll}C{\varepsilon}^{-\min\\{\beta_{0}/2,\alpha\\}}&\mbox{for}\
\displaystyle\int_{{\bf R}}g(x)dx\neq 0,\\\
C{\varepsilon}^{-\min\\{(\alpha+1)\beta_{0}/(\beta_{0}+2),\alpha\\}}&\mbox{for}\
\displaystyle\int_{{\bf R}}g(x)dx=0.\end{array}\right.$ (12)

We note that the second case in (12) gives us a new estimate when

$\alpha+1\leq\beta_{0}<2\alpha,$

because this restriction yields that

$\widetilde{T}({\varepsilon})\geq
C{\varepsilon}^{-(\alpha+1)\beta_{0}/(\beta_{0}+2)}\quad\mbox{and}\quad\frac{(\alpha+1)\beta_{0}}{\beta_{0}+2}>\frac{\beta_{0}}{2}.$

Also the sharpness of this result can be verified by setting

$p=\alpha+1,\ q=0,\ r=\beta_{0}+1,$

or

$p+q=\alpha+1,\ r=\beta_{0}+1\ \mbox{with}\ q\neq 0$

in Theorem 1.

We shall omit the proof of Theorem 2, but point out that it is initiated by
that of Thereom 1, especially the key is how to split $L^{\infty}$ norm of the
solution itself according to the appropriate domains. Let us see it in the
next section.

###  2.4. Strategy of the proof of Theorem 1.

The key of our success to prove the generalized combined effect case,
especially the existence part of (8), in Theorem 1 is to handle the system of
integral equations of $(u-{\varepsilon}u^{0},u_{t}-{\varepsilon}u^{0}_{t})$,
where $u^{0}$ is a solution of the free wave equation with the same initial
data $(u,u_{t})|_{t=0}=(f,g)$;

$u^{0}(x,t)=\frac{1}{2}\\{f(x+t)+f(x-t)\\}+\frac{1}{2}\int_{x-t}^{x+t}g(y)dy.$
(13)

The basic argument is due to John [7] in which classical solutions of
semilinear wave equations in three space dimensions are constructed in a
weighted $L^{\infty}$ space.

Assume that

$\mbox{supp}\ f,g\subset\\{|x|\leq R\\}\ \mbox{with}\ R>1,$ (14)

which yields that the finiteness of the propagation seed of the wave,

$\mbox{supp\ }u(x,t)\subset\\{|x|\leq t+R\\}$ (15)

by standard argument on small solutions of nonlinear wave equations. For
example, see Appendix in John [8]. Then, set an “interior” domain $D$ by

$D:=\\{t-|x|\geq R\\}$

and define a sequence $\\{(U_{j},V_{j})\\}$ by

$\left\\{\begin{array}[]{l}U_{j+1}=L(A_{0}|V_{j}+{\varepsilon}u_{t}^{0}|^{p}|U_{j}+{\varepsilon}u^{0}|^{q}+B_{0}|U_{j}+{\varepsilon}u^{0}|^{r}),\\\
U_{1}=0,\\\
V_{j+1}=L^{\prime}(A_{0}|V_{j}+{\varepsilon}u_{t}^{0}|^{p}|U_{j}+{\varepsilon}u^{0}|^{q}+B_{0}|U_{j}+{\varepsilon}u^{0}|^{r}),\\\
V_{1}=0,\end{array}\right.$

where $L(v)$ for a function $v$ of space-time variables is from Duhamel’s term
defined by

$\begin{array}[]{l}\displaystyle
L(v)(x,t):=\frac{1}{2}\int_{0}^{t}ds\int_{x-t+s}^{x+t-s}v(y,s)dy,\\\
\displaystyle L^{\prime}(v)(x,t):=\frac{\partial}{\partial
t}L(v)(x,t).\end{array}$ (16)

This sequence $\\{(U_{j},V_{j})\\}$ will converge to
$(u-{\varepsilon}u^{0},u_{t}-{\varepsilon}u_{t}^{0})$ in a function space

$\begin{array}[]{ll}X:=&\\{(U,V)\in\\{C^{1}({\bf R}\times[0,T])\\}^{2}\\\
&\quad:\|(U,V)\|_{X}<\infty,\ \mbox{supp}\ (U,V)\subset\\{|x|\leq
t+R\\}\\},\end{array}$

where

$\begin{array}[]{l}\|(U,V)\|_{X}:=\|U\|_{1}+\|U_{x}\|_{1}+\|V\|_{2}+\|V_{x}\|_{2},\\\
\|U\|_{1}:=\displaystyle\sup_{(x,t)\in{\bf
R}\times[0,T]}(t+|x|+R)^{-1}|U(x,t)|,\\\
\|V\|_{2}:=\displaystyle\sup_{(x,t)\in{\bf R}\times[0,T]}\\{\chi_{D}(x,t)\\\
\qquad+(1-\chi_{D}(x,t))(t+|x|+R)^{-1}\\}|V(x,t)|\end{array}$

and $\chi_{D}$ is a characteristic function of the interior domain $D$. In
view of the expression of $u^{0}$ in (13), it follows from (14) and the
assumption on $g$ yield the strong Huygens’ principle,

$u^{0}(x,t)\equiv\int_{{\bf R}}g(x)dx=0\quad\mbox{in}\ D.$ (17)

Then we have main a priori estimates;

$\begin{array}[]{ll}\|L(|V|^{p}|U|^{q})\|_{1}\leq
C\|V\|_{2}^{p}\|U\|_{1}^{q}(T+R)^{p+q},\\\ \|L(|U|^{r})\|_{1}\leq
C\|U\|_{1}^{r}(T+R)^{r+1},\\\ \|L^{\prime}(|V|^{p}|U|^{q})\|_{2}\leq
C\|V\|_{2}^{p}\|U\|_{1}^{q}(T+R)^{p+q},\\\ \|L^{\prime}(U|^{r})\|_{2}\leq
C\|U\|_{1}^{r}(T+R)^{r+1}\end{array}$

with some positive constant $C$ independent of ${\varepsilon}$ and $T$ which
give us the key estimates for $p+q<r$;

$\begin{array}[]{ll}\|U_{j+1}\|_{1}\lesssim&{\varepsilon}^{p+q}+\|V_{j}\|_{2}^{p}\|U_{j}\|_{1}^{q}T^{p+q}+\|U_{j}\|_{1}^{r}T^{r+1}+\mbox{harmless
terms},\\\ \|V_{j+1}\|_{2}\lesssim&\mbox{the same as above},\end{array}$

where $\lesssim$ stands for mod constant independent of ${\varepsilon}$ and
$T$. Therefore the boundedness of the sequence,
$\|U_{j}\|_{1},\|V_{j}\|_{2}\lesssim{\varepsilon}^{p+q}$ for all $j\in{\bf
N}$, follows from the competition between the second and third terms in the
right-hand side. When $(r+1)/2<p+q$, the third term is major, so that

${\varepsilon}^{r(p+q)}T^{r+1}\lesssim{\varepsilon}^{p+q}$

is the required condition. The difference to convergence of the sequence as
well as those for the spatial derivative is almost the same as the boundedness
above. Therefore we obtain the desired lower bound;

$T({\varepsilon})\geq C{\varepsilon}^{-(p+q)(r-1)/(r+1)}.$

For the upper bound in this generalized combined effect, its proof is easy if
we follow the argument by higher dimensional case by Han and Zhou [4]. In
fact, assume that $f(x)\geq 0(\not\equiv 0),\ g(x)\equiv 0$. Set

$F(t):=\displaystyle\int_{{\bf R}}u(x,t)dx.$

Then, the equation and (15) imply that

$F^{\prime\prime}(t)=\int_{{\bf R}}(A_{0}|u_{t}|^{p}|u|^{q}+B_{0}|u|^{r})dx.$

The second term and Hölder’s inequality yield that

$F^{\prime\prime}(t)\gtrsim(t+R)^{-(r-1)}|F(x)|^{r}\quad\mbox{for}\ t\geq 0.$
(18)

This is the main inequality. Next we shall make use of the first term to
obtain the better estimate than the single term. For this purpose, assume
further that

$f(x),-f^{\prime}(x)\geq\exists c>0\ \quad\mbox{for}\ x\in(-R/2,0).$

Then, we have that

$\left\\{\begin{array}[]{l}u(x,t)\gtrsim{\varepsilon}f(x-t)\gtrsim{\varepsilon},\\\
u_{t}(x,t)\gtrsim-{\varepsilon}f^{\prime}(x-t)\gtrsim{\varepsilon}\end{array}\right.\mbox{for}\
t<x<t+R.$

Plugging these estimates into the first term in (18), we obtain that

$F^{\prime\prime}(t)\gtrsim{\varepsilon}^{p+q}\quad\mbox{for large $t$}$

which implies that

$F(t)\gtrsim{\varepsilon}^{p+q}t^{2}\quad\mbox{for large $t$}.$ (19)

These estimates (18) and (19) will give us the desired result according to the
improved Kato’s lemma by Takamura [30]. But here we show a brief feeling that
the result is correct as follows. Plugging (19) into (18), we obtain that

$\begin{array}[]{l}F^{\prime\prime}(t)\gtrsim{\varepsilon}^{r(p+q)}t^{r+1}\quad\mbox{for
large $t$}\end{array}$

which implies that

$\begin{array}[]{l}F(t)\gtrsim{\varepsilon}^{r(p+q)}t^{r+3}\quad\mbox{for
large $t$}.\end{array}$ (20)

The difference of the lower bound of $F$ between (19) and (20) is

${\varepsilon}^{(p+q)(r-1)}t^{r+1}.$

This quantity is larger than some constant, we will reach to the desired
lifespan estimate

$T({\varepsilon})\leq C{\varepsilon}^{-(p+q)(r-1)/(r+1)}$

by standard iteration argument. Because we don’t have to cut the time interval
in each step, which means that this procedure can be repeated infinitely many
times in the fixed time interval. In this way, we obtain the sharp estimate of
the lifespan in the generalized combined effect case.

Other cases except for the generalized combined effect are similar to those
above. However, we point out that the existence part under the assumption of
$\displaystyle\int_{{\bf R}}g(x)dx\neq 0$ is most difficult practically among
all the proofs in choosing appropriate weight functions.

##  3\. The case of variable coefficients

In this section, we assume for our model (3) that $A(x,t)$, or $B(x,t)$, is of

$\frac{1}{\langle t+\langle x\rangle\rangle^{1+a}\langle t-\langle
x\rangle\rangle^{1+b}\langle x\rangle^{1+c}},\ \mbox{or}\ \equiv 0,$

where $a,b,c\in{\bf R}$ and $\langle x\rangle:=\sqrt{1+x^{2}}$. The reason to
take many $\langle\ \rangle$s is to ensure the differentiability of $A,B$ to
construct a classical solution. We will see that this kind of models will be a
key in extending the general theory for (1) to the non-autonomous terms as
stated at the end of Introduction. The weights of this kind were firstly
introduced by Belchev, Kepka and Zhou [2], later Liu and Zhou [17] in higher
space dimensions to show a blow-up result. But they set a special weight to
make use of some geometric transform to absorb it, and reduced the equation to
ordinary differential inequality of the functional without any argument on the
local existence of the solution as well as the lifespan estimates.

###  3.1. Motivation of the problem

Our motivation to consider such $A$ and $B$ above comes from an initial value
problem for the semilinear damped wave equations;

$\left\\{\begin{array}[]{ll}\displaystyle
v_{tt}-v_{xx}+\frac{2}{1+t}v_{t}=|v|^{p}&\quad\mbox{in}\ {\bf
R}\times(0,\infty),\\\ v(x,0)={\varepsilon}f(x),\quad
v_{t}(x,0)={\varepsilon}g(x)&\quad\mbox{for}\ x\in{\bf R}\end{array}\right.$
(21)

with the same setting on the initial data. This problem is a very important
model as it has a critical decay in damping term, namely scaling invariant
damping. The time-decay $(1+t)^{-1}$ is a threshold between heat-like with
weaker decay and wave-like with stronger decay in the sense that the each
critical exponent is the same as Fujita one and Strauss one respectively. In
the critical case, the size of the constant in front of the damping term is
important. There is also a threshold on the constant and this case “2” is in
the domain of heat-like in one dimension. See the introduction of Kato,
Takamura and Wakasa [10] for precise results and references. In fact,
D’Abbicco [1] showed for $p>3$ that the energy solution of (21) exists
globally-in-time, while Wakasugi [33] obtained its counter part of finite-time
blow-up of the energy solution for $1<p\leq 3$. This critical exponent $3$ is
Fujita one in one space dimension, so one may expect that the solution behaves
like one of semilinear heat equations for which $u_{tt}$ is neglected from
(21). But, this is not true.

In fact, Liouville transform $u(x,t)=(1+t)v(x,t)$ shows that (21) is
equivalent to

$\left\\{\begin{array}[]{ll}\displaystyle
u_{tt}-u_{xx}=\frac{|u|^{p}}{(1+t)^{p-1}}&\mbox{in}\ {\bf
R}\times(0,\infty),\\\ u(x,0)={\varepsilon}f(x),\
u_{t}(x,0)={\varepsilon}\\{f(x)+g(x)\\}&\mbox{for}\ x\in{\bf
R},\end{array}\right.$ (22)

so that all the technique for semilinear wave equations are applicable to this
problem, and we have the following results on the lifepsan estimates for (21).
Wakasa [31] obtained that

$\begin{array}[]{c}T({\varepsilon})\sim\left\\{\begin{array}[]{lll}C{\varepsilon}^{-(p-1)/(3-p)}&\mbox{for}&\displaystyle
1<p<3,\\\ \exp(C{\varepsilon}^{-(p-1)})&\mbox{for}&\displaystyle p=3\\\
\end{array}\right.\\\ \mbox{if}\ \displaystyle\int_{{\bf
R}}\\{f(x)+g(x)\\}dx\neq 0\end{array}$ (23)

This is the heat-like estimate in the sense that it coincides with the
corresponding semilinear heat equations for which $u_{xx}$ is neglected in
(21). In the original paper [31], the condition on the initial data is
missing, but it was expected to be natural as the critical exponent is Fujita
one. Later, Kato, Takamura and Wakasa [10] proved that

$\begin{array}[]{c}T({\varepsilon})\sim\left\\{\begin{array}[]{lll}C{\varepsilon}^{-p(p-1)/(1+2p-p^{2})}&\mbox{for}&\displaystyle
1<p<2,\\\ Cb({\varepsilon})&\mbox{for}&\displaystyle p=2,\\\
C{\varepsilon}^{-p(p-1)/(3-p)}&\mbox{for}&\displaystyle 2<p<3,\\\
\exp(C{\varepsilon}^{-p(p-1)})&\mbox{for}&\displaystyle
p=3\end{array}\right.\\\ \mbox{if}\ \displaystyle\int_{{\bf
R}}\\{f(x)+g(x)\\}dx=0,\end{array}$ (24)

where $b=b({\varepsilon})$ is a positive number satisfying
${\varepsilon}^{2}b\log(1+b)=1$. This is the wave-like estimate. In deed, the
cases $1<p<2$ and $p=3$ are the same forms as those of 3-dimensional
semillinear wave equations.

In this way, it is very important to study the weighted nonlinear terms, and
it is natural to extend the results to more general weighted terms than (22).
The first simple question may go to the case of $x$-decay.

###  3.2. Spatially weighted nonlinear terms.

First we consider the following case of spatial weights;

$A(x,t)\equiv 0\quad\mbox{and}\quad B(x,t)=\frac{1}{\langle x\rangle^{1+c}},$
(25)

where $c\in{\bf R}$, in (3). This setting was first introduced by Suzuki [28]
under the supervision by Prof. M. Ohta (Tokyo Univ. of Sci. Japan), but with
the assumption that the initial data is of non-compact support. Later, Kubo,
Osaka and Yazici [16] improved the result and Wakasa [32] finalized it. For
the compactly supported case, we have the following result.

######  Theorem 3 (Kitamura, Morisawa and Takamura [13]).

Assume (25). Then, the lifespan of a classical solution of (3) satisfies the
following estimates.

$T({\varepsilon})\sim\left\\{\begin{array}[]{ll}C{\varepsilon}^{-(p-1)/(1-c)}&\mbox{for}\
c<0,\\\ \phi^{-1}(C{\varepsilon}^{-(p-1)})&\mbox{for}\ c=0,\\\
C{\varepsilon}^{-(p-1)}&\mbox{for}\ c>0\end{array}\right.\quad\mbox{if}\
\int_{\bf R}g(x)dx\neq 0$ (26)

and

$T({\varepsilon})\sim\left\\{\begin{array}[]{ll}C{\varepsilon}^{-p(p-1)/(1-pc)}&\mbox{for}\
c<0,\\\ \psi^{-1}(C{\varepsilon}^{-p(p-1)})&\mbox{for}\ c=0,\\\
C{\varepsilon}^{-p(p-1)}&\mbox{for}\ c>0\end{array}\right.\quad\mbox{if}\
\int_{\bf R}g(x)dx=0,$ (27)

where $\phi^{-1}$ and $\psi^{-1}$ are inverse functions defined by
$\phi(s)=s\log(2+s)$ and $\psi(s)=s\log^{p}(2+s)$, respectively.

######  Remark 1.

Wakasa [32] established the estimate in (26) with the assumption that $f\in
L^{\infty}({\bf R}),\ g\in L^{1}({\bf R})$ and $c\geq-1$. The last condition
ensures the existence of local-in-time solutions with non-compactly supported
data. We also remark that $|u|^{p}$ in the nonlinear term can be replaced with
$|u|^{p-1}u$ in [32] due to the fact that the positiveness of the solution can
be obtained easier than the compactly supported case.

The strategy of the proof of Theorem 3 for the existence part is similar to
the one of Theorem 1 based on weighted $L^{\infty}$ estimates of the solution,
so we don’t comment about it here. For the blow-up part, the iteration
argument of the point-wise estimate is employed. The functional method like
could not applied.

After the work [13], one may study the counter case of

$A(x,t)=\frac{1}{\langle x\rangle^{1+c}}\quad\mbox{and}\quad B(x,t)\equiv 0,$
(28)

where $c\in{\bf R}$, in (3) with $q=0$. For this equation, one may expect that
the result is not so interesting as $|x|\sim t$ in dealing with the nonlinear
term $|u_{t}|^{p}$. But the result is

######  Theorem 4 (Zhou [37], Kitamura, Morisawa and Takamura [14]).

Assume (28) with $q=0$. Then, the lifespan of a classical solution of (3)
satisfies the following estimates.

$\begin{array}[]{l}T({\varepsilon})\sim\left\\{\begin{array}[]{ll}C{\varepsilon}^{-(p-1)/(-c)}&\mbox{for}\
c<0,\\\ \exp(C{\varepsilon}^{-(p-1)})&\mbox{for}\ c=0,\end{array}\right.\\\
T({\varepsilon})=\infty\quad\mbox{for}\ c>0.\end{array}$ (29)

We note that Zhou [37] established the blow-up part with $c=-1$, namely non-
weighted case. The proof of Theorem 4 is similar to the one of Theorem 3, so
we don’t comment about it here also. The main difference between (25) and (28)
is a possibility to obtain the global-in-time existence for (28) while there
is no such a situation due to the effect of the origin in space for (25).

According to the result on (21) and Theorems 3 and 4, one may expect that it
is sufficient to study the weights in the nonlinear terms by powers of $(1+t)$
or $\langle x\rangle$ for the purpose to extend the general theory, but we
have to take into account of “characteristic weights” in handling nonlinear
wave equations. Let’s see it in the next subsection.

###  3.3. Weighted nonlinear terms in the characteristic directions.

It is well-known that the wave propagates along with the characteristic
directions, so that it is not sufficient to study the weights of powers by
$(1+t)$ or $\langle x\rangle$ only. Therefore, as a breakthrough to this
direction, we set

$A(x,t)\equiv 0\quad\mbox{and}\quad B(x,t)=\frac{1}{\langle t+\langle
x\rangle\rangle^{1+a}\langle t-\langle x\rangle\rangle^{1+b}},$ (30)

where $a,b\in{\bf R}$, in (3). Then, we obtained the following result.

######  Theorem 5 (Kitamura, Wakasa and Takamura [15]).

Assume (30). Then, the lifespan $T({\varepsilon})$ of the classical solution
of (3) satisfies the following estimates;

$T({\varepsilon})=\infty\quad\mbox{for}\ a+b>0\ \mbox{and}\ a>0,$ (31)

and

$T({\varepsilon})\sim\left\\{\begin{array}[]{lllll}\exp(C{\varepsilon}^{-(p-1)})&\mbox{for}&\begin{array}[]{l}a+b=0\
\mbox{and}\ a>0,\\\ \mbox{or}\ a=0\ \mbox{and}\ b>0,\end{array}\\\
\exp(C{\varepsilon}^{-(p-1)/2})&\mbox{for}&a=b=0,\\\
C{\varepsilon}^{-(p-1)/(-a)}&\mbox{for}&a<0\ \mbox{and}\ b>0,\\\
\phi_{1}^{-1}(C{\varepsilon}^{-(p-1)})&\mbox{for}&a<0\ \mbox{and}\ b=0,\\\
C{\varepsilon}^{-(p-1)/(-a-b)}&\mbox{for}&a+b<0\ \mbox{and}\ b<0\\\
\end{array}\right.$ (32)

if

$\int_{{\bf R}}g(x)dx\neq 0,$

where $\phi_{1}^{-1}$ is an inverse function defined by

$\phi_{1}(s)=s^{-a}\log(2+s).$ (33)

On the other hand, it holds that

$T({\varepsilon})\sim\left\\{\begin{array}[]{lllll}\exp(C{\varepsilon}^{-(p-1)})&\mbox{for}&a=0\
\mbox{and}\ b>0,\\\ \exp(C{\varepsilon}^{-p(p-1)})&\mbox{for}&a+b=0\
\mbox{and}\ a>0,\\\ \exp(C{\varepsilon}^{-p(p-1)/(p+1)})&\mbox{for}&a=b=0,\\\
C{\varepsilon}^{-(p-1)/(-a)}&\mbox{for}&a<0\ \mbox{and}\ b>0,\\\
\psi_{1}^{-1}(C{\varepsilon}^{-p(p-1)})&\mbox{for}&a<0\ \mbox{and}\ b=0,\\\
C{\varepsilon}^{-p(p-1)/(-pa-b)}&\mbox{for}&a<0\ \mbox{and}\ b<0,\\\
\psi_{2}^{-1}(C{\varepsilon}^{-p(p-1)})&\mbox{for}&a=0\ \mbox{and}\ b<0,\\\
C{\varepsilon}^{-p(p-1)/(-a-b)}&\mbox{for}&a+b<0\ \mbox{and}\
a>0\end{array}\right.$ (34)

if

$\int_{{\bf R}}g(x)dx=0,$

where $\psi_{1}^{-1}$ and $\psi_{2}^{-1}$ are inverse functions defined by

$\psi_{1}(s)=s^{-pa}\log(2+s)\ \mbox{and}\ \psi_{2}(s)=s^{-b}\log^{p-1}(2+s).$
(35)

######  Remark 2.

The estimates (34) with $a=p-2$ and $b=-1$ coincide with (23) and (24) because
$(1+t)$ is equivalent to ${\langle{t+{\langle{x}\rangle}}\rangle}$ by finite
propagation speed of the wave like (15).

The strategy of the proof of Theorem 5 is also almost the same as the one of
Theorem 3, but the weights cause many technical difficulties, but we shall
skip the details fot the purpose of this paper. The main concern of Theorem 5
is that we have interactions among two characteristic directions as the
critical line $a+b=0$ with $b\leq 0$ and $a=0$ with $b\geq 0$ which divides
$ab$-plane into two domains of the global-in-time existence and the blow-up in
finite time.

In contrast, if

$A(x,t)=\frac{1}{\langle t+\langle x\rangle\rangle^{1+a}\langle t-\langle
x\rangle\rangle^{1+b}}\quad\mbox{and}\quad B(x,t)\equiv 0,$ (36)

where $a,b\in{\bf R}$, in (3) with $q=0$, then we obtained the different
critical line on $ab$-plane from Theorem 5 as follows.

######  Theorem 6 (Kitamura [12]).

Assume (28) with $q=0$. Then, the lifespan of a classical solution of (3)
satisfies the following estimates.

$\begin{array}[]{l}T({\varepsilon})\sim\left\\{\begin{array}[]{l}C{\varepsilon}^{-(p-1)/(-a)}\\\
\qquad\mbox{for}\ a<0\ \mbox{and}\ b\geq-p,\\\
C{\varepsilon}^{-p(p-1)/\\{-p(1+a)-b\\}}\\\ \qquad\mbox{for}\ p(1+a)+b<0\
\mbox{and}\ b<-p,\\\ \exp(C{\varepsilon}^{-(p-1)})\\\ \qquad\mbox{for}\ a=0\
\mbox{and}\ b\geq-p,\\\ \exp(C{\varepsilon}^{p(p-1)})\\\ \qquad\mbox{for}\
a>0\ \mbox{and}\ p(1+a)+b=0,\end{array}\right.\\\
T({\varepsilon})=\infty\quad\mbox{for}\ a>0\ \mbox{and}\
p(1+a)+b>0.\end{array}$ (37)

We note again that all the estimates above are established whatever the value
of $\displaystyle\int_{{\bf R}}g(x)dx$ is, due to the nonlinear term
$|u_{t}|^{p}$. The strategy of the proof of Theorem 6 is also almost the same
as the one of Theorem 3.

Concluding remark The series of our theorems above are major if one intends to
extend the general theory for non-autonomous equations. But they are not
sufficient still as we never try to analyze the combined effect for variable
coefficients case including the different order of $A$ and $B$.

###  3.4. Other models.

Finally we shall comment on the different nonlinear terms. Recently we
obtained the following result.

######  Theorem 7 (Sasaki, Takamatsu and Takamura [27]).

Assume that $A\equiv 1,B\equiv 0,q=0$ in (3). Moreover, $|u_{t}|^{p}$ is
replaced with $|u_{x}|^{p}$. Then we have that

$T({\varepsilon})\sim C{\varepsilon}^{-(p-1)}.$ (38)

One may feels that this result is trivial according to Theorem 3 with $c=-1$.
But the proof is different from each others. Especially there is a difficulty
on the blow-up part as the point-wise positivity of $u_{x}$ cannot be obtained
by

$\frac{\partial}{\partial x}L(v)(x,t),$

where $L(v)$ is the one in (16). This situation is overcome by taking suitably
weighted functional of the solution which was introduced by Rammaha [25, 26].
We believe that Theorem 7 will contribute to analysis of the “blow-up
boundary” for the equation

$u_{tt}-u_{xx}=|u_{x}|^{p}$

for which there is no result til now. See [27] for references therein to the
blow-up boundary.

## References

  * [1] M. D’Abbicco, The threshold of effective damping for semilinear wave equations, Mathematical Methods in Applied Sciences, 38 (2015), 1032-1045.
  * [2] E. Belchev, M. Kepka and Z. Zhou, Finite-time blow-up of solutions to semilinear wave equations, Special issue dedicated to the memory of I. E. Segal. J. Funct. Anal. 190 (2002), no. 1, 233-254.
  * [3] W. Dai, D. Fang and C. Wang, Global existence and lifespan for semilinear wave equations with mixed nonlinear terms, J. Differential Equations, 267 (2019), no. 5, 3228-3354.
  * [4] W. Han and Y. Zhou, Blow up for some semilinear wave equations in multi-space dimensions, Comm. Partial Differential Equations, 39 (2014), no. 4, 651-665.
  * [5] K. Hidano, C. Wang and K. Yokoyama, Combined effects of two nonlinearities in lifespan of small solutions to semi-linear wave equations, Math. Ann., 366 (2016), no. 1-2, 667-694.
  * [6] T. Imai, M. Kato, H. Takamura and K. Wakasa, The sharp lower bound of the lifespan of solutions to semilinear wave equations with low powers in two space dimensions, Asymptotic analysis for nonlinear dispersive and wave equations, 31-53, Adv. Stud. Pure Math., 81, Math. Soc. Japan, Tokyo, 2019.
  * [7] F. John, Blow-up of solutions of nonlinear wave equations in three space dimensions, Manuscripta Math., 28 (1979), no. 1-3, 235-268.
  * [8] F. John, “Nonlinear Wave Equations, Formation of Singularities”, ULS Pitcher Lectures in Mathematical Science, Lehigh University, American Mathematical Society, Providence, RI, 1990.
  * [9] S. Katayama, Lifespan of solutions for two space dimensional wave equations with cubic nonlinearity, Comm. Partial Differential Equations, 26 (2001), no. 1-2, 205-232.
  * [10] M. Kato, H. Takamura and K. Wakasa, The lifespan of solutions of semilinear wave equations with the scale-invariant damping in one space dimension, Differential Integral Equations, 32 (2019), no. 11-12, 659-678.
  * [11] R. Kido, T. Sasaki, S. Takamatsu and H. Takamura, The generalized combined effect for one dimensional wave equations with semilinear terms including product type, arXiv:2305.00180.
  * [12] S. Kitamura, Semilinear wave equations of derivative type with characteristic weights in one space dimension, arXiv:2211.12295.
  * [13] S. Kitamura, K. Morisawa and H. Takamura, The lifespan of classical solutions of semilinear wave equations with spatial weights and compactly supported data in one space dimension, J. Differential Equations, 307 (2022), 486-516.
  * [14] S. Kitamura, K. Morisawa and H. Takamura, Semilinear wave equations of derivative type with spatial weights in one space dimension, Nonlinear Analysis, RWA, 72 (2023), Paper No.103764.
  * [15] S. Kitamura, H. Takamura and K. Wakasa, The lifespan estimates of classical solutions of one dimensional semilinear wave equations with characteristic weights, J. Math. Anal. Appl. 528 (2023), Paper No. 127516.
  * [16] H. Kubo, A.Osaka and M.Yazici, Global existence and blow-up for wave equations with weighted nonlinear terms in one space dimension, Interdisciplinary Information Sciences, 19 (2013), 143-148.
  * [17] X. Liu and Y. Zhou, Global nonexistence of solutions to a semilinear wave equation in the Minkowski space, Appl. Math. Lett. 21 (2008), no. 8, 849-854.
  * [18] T.-T. Li (D.-Q. Li), X. Yu and Y. Zhou, Durée de vie des solutions régulières pour les équations des ondes non linéaires unidimensionnelles (French), C. R. Acad. Sci. Paris Sér. I Math., 312 (1991), no. 1, 103-105.
  * [19] T.-T. Li, X. Yu and Y. Zhou, Life-span of classical solutions to one-dimensional nonlinear wave equations, Chinese Ann. Math., Ser. B, 13 (1992), no. 3, 266-279.
  * [20] M. Liu and C. Wang, Blow up for small-amplitude semilinear wave equations with mixed nonlinearities on asymptotically Euclidean manifolds, J. Differential Equations, 269 (2020), no. 10, 8573-8596.
  * [21] G. K. Luli, S. Yang, P. Yu, On one-dimension semi-linear wave equations with null conditions, Adv. Math., 329 (2018), 174-188.
  * [22] M. Nakamura, Remarks on a weighted energy estimate and its application to nonlinear wave equations in one space dimension, J. Differential Equations, 256, no. 2, (2014), 389-406.
  * [23] K. Morisawa, T. Sasaki and H. Takamura, The combined effect in one space dimension beyond the general theory for nonlinear wave equations, Comm. Pure Appl. Anal., 22 (2023), no. 5, 1629-1658.
  * [24] K. Morisawa, T. Sasaki and H. Takamura, Erratum to “The combined effect in one space dimension beyond the general theory for nonlinear wave equations”, to appear in Comm. Pure Appl. Anal.
  * [25] M. A. Rammaha, Upper bounds for the life span of solutions to systems of nonlinear wave equations in two and three space dimensions, Nonlinear Anal. 25 (1995), no. 6, 639-654.
  * [26] M. A. Rammaha, A note on a nonlinear wave equation in two and three space dimensions, Comm. Partial Differential Equations 22 (1997), no. 5-6, 799-810.
  * [27] T. Sasaki S. Takamatsu and H. Takamura, The lifespan of classical solutions of one dimensional wave equations with semilinear terms of the spatial derivative, AIMS Math., 8, no. 11, 25477-25486.
  * [28] A. Suzuki, “Global Existence and Blow-Up of solutions to Nonlinear Wave Equations in One Space Dimension” (in Japanese), Master Thesis, Saitama University, 2010.
  * [29] S. Takamatsu, Improvement of the general theory for one dimensional nonlinear wave equations related to the combined effect, arXiv: 2308.02174.
  * [30] H. Takamura, Improved Kato’s lemma on ordinary differential inequality and its applications to semilinear wave equations, Nonlinear Anal., 125 (2015), 227-240.
  * [31] K. Wakasa, The lifespan of solutions to semilinear damped wave equations in one space dimension, Communications on Pure and Applied Analysis, 15 (2016), 1265-1283.
  * [32] K. Wakasa, The lifespan of solutions to wave equations with weighted nonlinear terms in one space dimension, Hokkaido Math. J., 46 (2017), 257-276.
  * [33] Y. Wakasugi, Critical exponent for the semilinear wave equation with scale invariant damping, Fourier analysis, 375-390, Trends Math., Birkhäuser/Springer, Cham, 2014.
  * [34] D. Zha, On one-dimension quasilinear wave equations with null conditions, Calc. Var. Partial Differential Equations, 59 (2020), no. 3, Paper No. 94, 19 pp.
  * [35] D. Zha, Global stability of solutions to two-dimension and one-dimension systems of semilinear wave equations, J. Funct. Anal., 282 (2022), no. 1, Paper No. 1092219, 26 pp.
  * [36] Y. Zhou, Life span of classical solutions to $u_{tt}-u_{xx}=|u|^{1+\alpha}$, Chinese Ann. Math. Ser.B, 13 (1992), no. 2, 230-243.
  * [37] Y. Zhou, Blow up of solutions to the Cauchy problem for nonlinear wave equations, Chinese Ann. Math. Ser. B, 22 (2001), no. 3, 275-280.
  * [38] Y. Zhou, Blow up of solutions to the Cauchy problem for nonlinear wave equations, preprint, Fudan University, 1992.