CST4-nocomments.tex
\documentclass[11pt,a4paper]{article}

\usepackage{amsmath,amsthm,amssymb,dsfont,paralist}
%
\usepackage{graphicx}

\newtheorem{df}{Definition}[section]
\newtheorem{lm}[df]{Lemma}
\newtheorem{ex}[df]{Example}
\newtheorem{prop}[df]{Proposition}
\newtheorem{theo}[df]{Theorem}
\newtheorem{cor}[df]{Corollary}
\newtheorem{ob}[df]{Observation}
\newtheorem{nt}[df]{Note}
\newtheorem{princ}[df]{Principle}
\newtheorem{alg}[df]{Algorithm}
\newtheorem{met}[df]{Method}
\newtheorem{fact}[df]{Fact}


\newcommand{\eat}[1]{}

\DeclareMathOperator{\MSO}{\mathrm{MSO}}
\DeclareMathOperator{\REMSO}{\mathrm{REMSO}}
\DeclareMathOperator{\FO}{\mathrm{FO}}
\DeclareMathOperator{\EMSO}{\mathrm{EMSO}}
\DeclareMathOperator{\PDA}{\mathrm{PDA}}
\DeclareMathOperator{\uPDA}{\mathrm{uPDA}}
\DeclareMathOperator{\ALG}{\mathrm{ALG}}
\DeclareMathOperator{\CF}{\mathrm{CF}}
\DeclareMathOperator{\uCF}{\mathrm{uCF}}
\DeclareMathOperator{\sRMSO}{\mathrm{srMSO}}
\DeclareMathOperator{\qfMSO}{\mathrm{qf-MSO}}
\DeclareMathOperator{\LTL}{\mathrm{LTL}}
\DeclareMathOperator{\Max}{\sf{Max}}
\DeclareMathOperator{\Last}{\sf{Last}}
\DeclareMathOperator{\Val}{\mathrm{val}}
\DeclareMathOperator{\Sup}{\sf{Sup}}

\DeclareMathOperator{\one}{\mathds{1}}
\DeclareMathOperator{\rec}{rec}
\DeclareMathOperator{\mso}{mso}
\DeclareMathOperator{\V}{{\cal V}}
\DeclareMathOperator{\La}{{\cal L}}
\DeclareMathOperator{\N}{\mathbb{N}}
\DeclareMathOperator{\pset}{{\cal P}}
\newcommand{\Nu}{\mathcal{V}}
\DeclareMathOperator{\Free}{\mathrm{Free}}
\DeclareMathOperator{\aeold}{\mathrm{oldest.\!ch}}
\DeclareMathOperator{\aeyoung}{\mathrm{youngest.\!ch}}
\DeclareMathOperator{\aenext}{\mathrm{ne}}
\DeclareMathOperator{\aeroot}{\mathrm{rt}}
\DeclareMathOperator{\aeleaf}{\mathrm{lf}}
\DeclareMathOperator{\pos}{pos}
\DeclareMathOperator{\dom}{dom}
\DeclareMathOperator{\rmin}{in}
\DeclareMathOperator{\wt}{wt}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\ttop}{top}
\DeclareMathOperator{\rest}{rest}
\DeclareMathOperator{\out}{out}
\DeclareMathOperator{\supp}{supp}
%
%
\DeclareMathOperator{\U}{\mathrm{U}}
\DeclareMathOperator{\X}{\mathrm{X}}
\DeclareMathOperator{\D}{\mathrm{D}}
\DeclareMathOperator{\sym}{\mathrm{sym}}
\DeclareMathOperator{\coeff}{\mathrm{coeff}}
\DeclareMathOperator{\lab}{\mathrm{lab}}

\newcommand{\gen}[1]{\langle #1\rangle}
\newcommand{\sem}[1]{[\![#1]\!]}

\newcommand{\eop}{$\Box$}
\newcommand{\nat}{\mathbb{N}}
\newcommand{\eps}{\varepsilon}
\newcommand{\vi}{\varphi}
\newcommand{\fl}{\langle \! \langle}
\newcommand{\fr}{\rangle \! \rangle}
\newcommand{\Bo}{\mathbb{B}}
\newcommand{\seml}{[\![}
\newcommand{\semr}{]\!]}
\newcommand{\beh}{|\!|}
\newcommand{\Y}{{\cal Y}}
\newcommand{\Yr}{{\cal Y}r}
\newcommand{\Ys}{{\cal Y}\#}
\newcommand{\I}{{\cal I}}
\newcommand{\J}{{\cal J}}
\newcommand{\G}{{\cal G}}
\newcommand{\M}{{\cal M}}
\newcommand{\HH}{{\cal H}}

\newcommand{\define}[1]{\emph{#1}}
\newcommand{\Real}{\mathbb{R}}

\providecommand*{\zero}    [0]{\ensuremath{\mathbf 0}}
\providecommand*{\one}     [0]{\ensuremath{\mathbf 1}}
\providecommand*{\sr}      [0]{\ensuremath{(K, \oplus,\odot,\zero,\one)}}
\providecommand*{\posr}    [0]{\ensuremath{(K,\oplus, \odot,\zero,\one,\leq)}}
\providecommand*{\srs}     [0]{\ensuremath{\mathcal K}}




\setlength{\textwidth}{158mm}
\newcounter{boxwidth}
\setcounter{boxwidth}{153}
\setlength{\parskip}{0.5mm}
\setlength{\parindent}{2mm}

\addtolength{\oddsidemargin}{-15mm}
\addtolength{\evensidemargin}{-28mm}
\addtolength{\topmargin}{-8mm}
%
\addtolength{\textheight}{12mm}
%
\parindent0em
\parskip0.3em


%
%
%
\let\s=\sigma
\let\d=\delta
\let\S=\Sigma
\let\R=\Delta
\def\-{$-$}
\def\|{\hspace{1mm} | \hspace{1mm}}
\def\ts{T_\Sigma}
\def\td{T_\Delta}
\def\les#1#2#3{#1\leq #2\leq #3}       %
\def\seq#1#2#3{#1_{#2},\ldots,#1_{#3}} %
\def\seqq#1#2#3#4{#1_{#3}(#2_{#3}),\ldots,#1_{#4}(#2_{#4})}
%
\def\red#1{\rightarrow_{#1}}
\def\tred#1{\rightarrow_{#1}^{*}}
\def\thue#1{\leftrightarrow_{#1}}
\def\tthue#1{\leftrightarrow_{#1}^{*}}
\def\der#1{\Rightarrow_{#1}}
\def\tder#1{\Rightarrow_{#1}^{*}}
\def\ttder#1{\Leftrightarrow_{#1}^{*}}
\def\mac{M=(Q,\S,\R,q_0,R)}
\def\att{A=(Att,\S,\R,\rho,a_0,R)}
\def\as{Att_{syn}}
\def\ai{Att_{inh}}
\def\mt{macro tree transducer\ }
\def\at{attributed tree transducer\ }
\let\c=\circ
\let\u=\cup
\def\g0{\geq0}             %
\let\b=\Box                %
\def\pr{\noindent{\bf Proof.\ }}
\let\vp=\varphi


\def\su#1#2#3#4{[#1_{#3}\leftarrow#2_{#3},\ldots,
                      #1_{#4}\leftarrow#2_{#4}]}
\def\ui#1{^{(#1)}}



\begin{document}
\begin{center}

{\LARGE The Chomsky-Sch\"utzenberger Theorem\\[3mm] for Quantitative Context-Free Languages}


\

\

\begin{tabular}{cc}
{\large Manfred Droste} & {\large Heiko Vogler}\\[1mm]
{\small {\it Institute of Computer Science}}
& {\small {\it Department of Computer Science}}\\[1mm]
{\small {\it Leipzig University}} & {\small {\it Technische
    Universit\"at Dresden}}\\[1mm]
{\small {\it D-04109 Leipzig, Germany}} & {\small {\it D-01062 Dresden, Germany}} \\[1mm]
{\small \tt droste@informatik.uni-leipzig.de} &
{\small \tt Heiko.Vogler@tu-dresden.de}
\end{tabular}

\

\today


\end{center}


\hyphenation{semi-rings}


\begin{quote}{\bf Abstract:}
Weighted automata model quantitative aspects of systems like the consumption of resources during executions.
Traditionally, the weights are assumed to form the algebraic structure of a semiring, but recently also other weight computations like average have been considered.
Here, we investigate quantitative context-free languages over very general weight structures incorporating all semirings, average computations, lattices, and more.
In our main result, we derive the fundamental Chomsky-Sch\"utzenberger theorem for such quantitative context-free languages, showing that each arises as the image of a Dyck language and a regular language under a suitable morphism.
Moreover, we show that quantitative context-free language are expressively equivalent to a model of weighted pushdown automata.
This generalizes results previously known only for semirings.
We also investigate when quantitative context-free languages assume only finitely many values.
\end{quote}



\section{Introduction}

The Chomsky-Sch\"utzenberger Theorem forms a famous cornerstone in the theory of context-free languages \cite{chosch63} relating arbitrary context-free languages to Dyck-languages and regular languages.
A weighted version of this result was presented in \cite{salsoi78} where the weights are taken from a commutative semiring. For surveys on this we refer the reader to \cite{autberboa97,petsal09}.

Recently, in \cite{chadoyhen09a,chadoyhen08,chadoyhen09,chadoyhen09b} new models of quantitative automata for technical systems have been investigated describing, e.g., the average consumption of resources.
In \cite{chavel12} pushdown automata with mean-payoff cost functions were considered which comprize a quantitative modelling of sequential programs with recursion. These cost functions cannot be computed in semirings.
Automata over the general algebraic structure of valuation monoids incorporating both semiring-weighted automata and quantitative automata were investigated in \cite{dromei10,dromei11}.

It is the goal of this paper to investigate weighted context-free grammars over valuation monoids. These include all semirings but we may also associate to each derivation, for instance, the average of the costs of the involved productions.
We could also associate with each production its  degree of sharpness or truth, as in multi-valued logics, using bounded lattices as valuation monoids.
Thereby, we can associate to each word over the underlying alphabet $\Sigma$ such a value (real number, element of a lattice, etc.) indicating its total cost or degree of truth, and any function from $\Sigma^*$  into the value set is called a quantitative language or series. Note that by the usual identification of sets with $\{0,1\}\,$-valued functions, classical languages arise as particular quantitative languages.


Now we give a summary of our results. We prove the equivalence of
weighted context-free grammars and weighted pushdown automata  over
arbitrary valuation monoids (cf. Theorem \ref{th:PDA=CF}). In our main result we
derive a weighted version of the Chomsky-Sch\"utzenberger Theorem
 over arbitrary valuation monoids (cf. Theorem \ref{th:char}). In particular, we show that any
 quantitative context-free language arises as the image of a
 Dyck-language and a regular language under a suitable weighted
 morphism. Conversely, each quantitative language arising
 as such an image is a quantitative context-free
 language. This shows that the weighted Chomsky-Sch\"utzenberger
 Theorem holds for much more general weighted structures than semirings,
 in particular, neither associativity, nor commutativity, nor
 distributivity of the multiplication are needed. The classical Chomsky-Sch\"utzenberger
 Theorem follows by considering the Boolean semiring $\{0,1\}$.

Finally we consider series which assume only finitely many values.
Such series were important in the context of recognizable series and weighted MSO logic (cf. \cite{berreu88,drogas07}).
In contrast to the setting of recognizable series, even over the semiring of natural numbers, characteristic series of inherently ambiguous context-free languages are not context-free (cf. Observation \ref{ex:inh-amb}).
Here we give sufficient conditions for obtaining context-freeness.
Conversely, we show that under suitable local finiteness conditions on the valuation monoid, each quantitative context-free language assumes just finitely many values, each on context-free languages, only.
These results seem to be new even for finite semirings.
As a consequence, weighted context-free languages over bounded lattices are context-free step functions.

In \cite{dromei11,mei11,dromei10}, two other fundamental results of formal language theory, the Kleene and B\"uchi theorem for regular languages, were shown to hold not only for semiring-weighted automata \cite{sch61,drostuvog10}, but also for quantitative automata over valuation monoids.
This raises the question which further results from the theory of semiring-weighted automata could be extended to more general quantitative automata settings including calculations of averages.






\section{Valuation Monoids and Series}
\label{sec:monoids-series}

A \emph{unital valuation monoid} is a tuple $(K,+,\Val,0,1)$ such that
\begin{compactenum}
\item $(K,+,0)$ is a commutative monoid,
\item $\Val: K^* \rightarrow K$ is a mapping such that $\Val(a) = a$ for each $a \in K$ and $\Val(\varepsilon) = 1$,
\item $\Val(a_1,\ldots, a_n) = 0$ whenever $a_i =0$ for some $1 \le i \le n$, and
\item $\Val(a_1,\ldots, a_{i-1},1,a_{i+1},\ldots, a_n) = \Val(a_1,\ldots, a_{i-1}
,a_{i+1},\ldots, a_n)$ for any $1 \le i \le n$.
\end{compactenum}
The concept of {\em valuation monoid} was introduced in
\cite{dromei10,dromei11} as a structure $(K,+,\Val,0)$ with a mapping  $\Val:  K^+ \rightarrow K$  satisfying requirements 1-3 correspondingly. In \cite{dromei10,dromei11,mei11}, also many examples of valuation monoids were given. For this paper, it will be important that the valuation monoids
contain a unit 1. We will see below in Example \ref{ex:val} that this means no restriction of generality.
Note that, similarly to sums where the element 0 is neutral and can be left out, $\Val$ can be considered as a very general product in which the unit 1 is neutral as reflected by requirement 4.


\begin{ex}\label{ex:val}\rm

1. \sloppy Let $(K,+,\Val,0)$ be a valuation monoid and let $1 \not\in K$. We put $K' = K \cup \{1\}$ and define $(K',+',\Val',0,1)$ such that $+'$ extends $+$, $x +' 1 = 1 +' x = 1$ for each $x \in K'$, and $\Val'(a_1,\ldots, a_n) = \Val(b_1,\ldots,b_m)$ where $b_1\ldots b_m$ is the subsequence of $a_1,\ldots, a_n$ excluding $1$'s. Then $(K',+',\Val',0,1)$ is a unital valuation monoid.

2. \sloppy The structure $(\mathbb{R} \cup \{-\infty\}, \sup, \mathrm{avg}, -\infty)$ with $\mathrm{avg}(a_1,\ldots,a_n) = \frac{1}{n} \cdot \sum_{i=1}^n a_i$ is a valuation monoid. Applying the procedure of Example 1 to it, we could add $\infty$ as the unit 1, disregarding $\infty$ when
calculating averages. This leads to a unital valuation monoid $(\mathbb{R} \cup \{-\infty,\infty\}, \sup, \mathrm{avg}, -\infty,\infty)$.

3.  Let $(K,+,\Val,0)$ be a valuation monoid. Note that in Example 1, the unit 1 satisfies $1+'1= 1$. Here we wish to give another extension of $K$ to a unital valuation monoid $K'$ which does not satisfy this law for $1$. Let $K' =  \mathbb{N} \times K$ with componentwise addition $+'$. Given $(m_1,x_1), \ldots, (m_n,x_n)$  we define $\Val'((m_1,x_1), \ldots, (m_n,x_n)) = \Val(x_1, \ldots, x_1, \ldots , x_n\ldots, x_n)$ where this sequence contains $m_i$ copies of $x_i$, if $m_i \not= 0$ and $x_i \not=0$ (for $1 \le i \le n$), otherwise the $x_i$'s are excluded from the sequence to which $\Val$ is applied.
Then $(K',+',\Val',(0,0),(1,0))$ is a unital valuation monoid. %



4. Next we introduce unital valuation monoids where the valuation arises from `local', binary operations as follows.  First, we define a \emph{unital monoid-magma} to be a tuple $(K,+,\cdot,0,1)$ such that $(K,+,0)$ is a commutative monoid, $\cdot:K\times K\rightarrow K$ is a binary operation, and $a \cdot 0 = 0 \cdot a = 0$ and $a \cdot 1 = 1 \cdot a = a$ for every $a \in K$.  Then we can consider each unital monoid-magna $(K,+,\cdot,0,1)$ as the particular unital valuation monoid $(K,+,\Val,0,1)$  where $\Val(a_1,\ldots, a_n) = (\ldots((a_1 \cdot a_2)\cdot a_3)\cdot \ldots )\cdot a_n$.
Now we list some examples of (classes of) unital monoid-magmas which can be viewed as unital valuation monoids in this way:
\begin{itemize}
\item A unital monoid-magma is a \emph{strong bimonoid}, if the multiplication is associative, and a \emph{semiring}, if the multiplication is associative and distributive (from both sides) over addition. For a range of examples of strong bimonoids which are not semirings we refer the reader to  \cite{drostuvog10}.

\item The Boolean semiring $\mathbb{B}=(\{0,1\},\lor,\land,0,1)$ allows us to give exact translations between unweighted and $\mathbb{B}$-weighted settings. The semiring $(\mathbb{N},+,\cdot,0,1)$ of natural numbers permits counting.


\item Each bounded lattice $(L,\lor,\land,0,1)$ (i.e. $0\le x\le 1$ for each $x\in L$) is a strong bimonoid. There is a wealth of lattices \cite{bir67,gra03} which are not distributive, hence strong bimonoids but not semirings.

\item
Let $(S,+,\cdot,0,1)$ be a strong bimonoid and let $n\ge 2$. Then the set of all $(n\times n)$-matrices over $S$ together with the usual pointwise addition and the usual multiplication of matrices forms a unital monoid-magma. We note that this matrix multiplication is not associative if the multiplication of the strong bimonoid is not distributive. We just note that such matrices arise naturally when considering the behavior of weighted automata over strong bimonoids, cf. \cite[p. 159]{drostuvog10}.


\item The structure $(\overline{\mathbb{R}},\sup,\mathrm{avg}_2,-\infty,\infty)$ with $\overline{\mathbb{R}}=\mathbb{R}\cup\{-\infty,\infty\}$, and $\mathrm{avg}_2(a,b)=\frac{a+b}{2}$ if $a,b<\infty$, $\mathrm{avg}_2(a,\infty)=\mathrm{avg}_2(\infty,a)=a$ ($a,b\in\overline{\mathbb{R}}$) is a unital monoid-magma, but not a strong bimonoid.

\end{itemize}
\end{ex}


The importance of infinitary sum operations was observed early on in weighted automata theory, cf. \cite{eil74}. In our context, they will arise for ambiguous context-free grammars if a given word has infinitely many derivations.

A monoid $(K,+,0)$ is {\em complete} \cite{eil74} if it has infinitary
sum operations $\sum_I:K^I \rightarrow K$ for any index set
$I$  such that $\sum_{i \in \emptyset} a_i = 0$, $\sum_{i \in \{k\}}
a_i = a_k$,  $\sum_{i \in \{j, k\}} a_i = a_j + a_k$ for $j\not= k$,
and $\sum_{j\in J} \left( \sum_{i \in I_j} a_i\right) = \sum_{i\in I}
a_i$ if $\bigcup_{j \in J} I_j = I$ and  $I_j \cap I_k = \emptyset$
for $j \not= k$.


A monoid $(K,+,0)$ is {\em idempotent} if $a+a=a$ for each $a \in K$,
and a complete monoid is {\em completely idempotent} if $\sum_{I} a =
a$ for each $a \in K$ and any index set $I$.

We call a unital valuation monoid $(K,+,\Val,0,1)$ complete,
idempotent, or completely idempotent if $(K,+,0)$ has the respective
property.



\begin{ex}
\rm 1. The Boolean semiring $\mathbb{B}$
  and the tropical semiring $(\mathbb{N}\cup \{\infty\}, \min,+,\infty,0)$
are complete and completely idempotent. For a wealth of further examples of complete semirings see
\cite[Ch.22]{gol99}.

2. The unital valuation monoid $(\mathbb{R}\cup \{-\infty,\infty\},
\sup,\mathrm{avg},-\infty,\infty)$ (cf. Example \ref{ex:val}(2)) is complete
and completely idempotent.

3. Consider the commutative monoid $(\{0,1,\infty\}, +,0)$  with
$1 +1 = 1$, $1 + \infty = \infty + \infty = \infty$, and $\sum_{I}1 =
\infty$ for any infinite index set $I$ and corresponding natural laws
for infinite sums involving the other elements. This monoid is complete
and idempotent, but not completely idempotent.
\end{ex}


Let $\Sigma$ be an alphabet and $K$ a unital valuation
monoid. A \emph{series} or \emph{quantitative language} over $\Sigma$ and $K$ is a mapping $s:
\Sigma^* \rightarrow K$. As usual, we denote $s(w)$ by $(s,w)$.
%
The \emph{support} of $s$ is the set $\supp(s) = \{w \in \Sigma^* \mid (s,w) \not= 0\}$. The \emph{image} of $s$ is the set $\im(s) = \{(s,w)\mid w \in \Sigma^*\}$.  The classes of all series over $\Sigma$ and $K$ is denoted by $K\fl \Sigma^*\fr$.

Let $s,s' \in K\fl \Sigma^*\fr$ be series.  We define the sum $s+s'$  by letting $(s+ s',w) = (s,w) + (s',w)$ for each $w \in \Sigma^*$. %

A family of series $(s_i \mid i \in I)$ is \emph{locally finite} if
for each $w \in \Sigma^*$ the set $I_w = \{i \in I \mid (s_i,w) \not=
0\}$ is finite. In this case or if $K$ is complete, we define $\sum_{i \in I} s_i \in K\fl \Sigma^*\fr$ by letting $(\sum_{i \in I} s_i, w) = \sum_{i \in I_w} (s_i,w)$ for every $w \in \Sigma^*$.

For $L \subseteq \Sigma^*$, we define the {\it characteristic series}
$\one_{L} \in K\fl \Sigma^*\fr$ by $(\one_L,w) = 1$ if $w \in L$, and
$(\one_L,w) = 0$ otherwise  for $w \in \Sigma^*$.


\begin{quote}\em In the rest of this paper, let $(K,+,\Val,0,1)$ denote an arbitrary unital valuation monoid, unless specified otherwise.
\end{quote}



\section{Weighted Context-Free Grammars}

In this section, we introduce our notion of weighted context-free grammars and we present basic properties. First we fix our notations for context-free grammars. Let $\Sigma$ be
an alphabet. A \emph{context-free grammar} (CFG) is a tuple
$\G = (N,\Sigma,Z,P)$ where $N$ is a finite set (\emph{nonterminals}),
$Z \in N$ (\emph{initial nonterminal}), and $P \subseteq_{f} N \times
(N \cup \Sigma)^*$ a finite set (\emph{productions}).

The leftmost derivation relation of $\G$  is the binary relation on the set $(N \cup \Sigma)^*$ of \emph{sentential forms} defined as follows. For every production $\rho = (A \rightarrow \xi) \in P$ we define the binary relation
\[
\stackrel{\rho}{\Rightarrow} (N \cup \Sigma)^* \times (N \cup \Sigma)^*
\]
such that for every $w \in \Sigma^*$ and $\zeta \in (N \cup \Sigma)^*$, we have
\[
w\, A \, \zeta \stackrel{\rho}{\Rightarrow} w \, \xi \, \zeta\enspace.
\]
The \emph{(leftmost) derivation relation} of $\G$ is the binary relation $\Rightarrow = \bigcup_{\rho\in P} \stackrel{\rho}{\Rightarrow}$.

A \emph{derivation} of $\G$ is a sequence $d = \rho_1\ldots\rho_n$ of
productions $\rho_i \in P$ such that there are sentential forms
$\xi_0,\ldots,\xi_n$ with $\xi_{i-1} \stackrel{\rho_i}{\Rightarrow}
\xi_i$ for every $1 \le i \le n$. We abbreviate this derivation by $\xi_0  \stackrel{d}{\Rightarrow} \xi_n$.
Let $A\in N$ and  $w \in \Sigma^*$. An \emph{$A$-derivation
  of $w$} is a derivation $d$ such that $A \stackrel{d}{\Rightarrow}
w$. We let $D(A,w)$ denote the set of all $A$-derivations
of $w$. And we let $D(w) = D(Z,w)$ denote the set of all {\em derivations of $w$}.

The \emph{language generated by $\G$} is the set
\[
L(\G) = \{w \in \Sigma^* \mid D(w) \not= \emptyset\}\enspace.
\]

We say that $\G$ is {\em ambiguous} if there is a $w \in L(\G)$ such that
$|D(w)| \ge 2$; otherwise $\G$ is {\em unambiguous}. A context-free
language $L$ is {\em inherently ambiguous} if every CFG $\G$ with $L =
L(\G)$ is ambiguous.

Due to the context-freeness of the rewriting we can observe the following easy decomposition of derivations.

\begin{ob}\label{ob:dec} Let $A \in N$, $w \in \Sigma^*$, and $d = \rho_1\ldots \rho_n \in D(A,w)$. Moreover, let $1 \le i \le n$ and $\rho_i =(B \rightarrow u_0B_1u_1\ldots B_ku_k)$. Then there are uniquely determined
\begin{compactitem}
\item $v_1,v_2 \in \Sigma^*$ and $\theta_1,\theta_2 \in P^*$ and
\item $w_1,\ldots,w_k \in \Sigma^*$ and $d_1\in D(B_1,w_1), \ldots , d_k\in D(B_k,w_k)$
\end{compactitem}
such that
\begin{compactitem}
\item $w = v_1 \, u_0w_1u_1\ldots w_ku_k \, v_2$,
\item $d = \theta_1 \, \rho_i d_1\ldots d_k \, \theta_2$, and
\item $\rho_id_1\ldots,d_k \in D(B,u_0w_1u_1\ldots w_ku_k)$.
\end{compactitem}
\end{ob}


Next let $K$ be a unital valuation monoid. A \emph{context-free grammar with weights} is a tuple $\G = (N,\Sigma,Z,P,\wt)$ where $(N,\Sigma,Z,P)$ is a CFG and $\wt: P \rightarrow K$ is a mapping (\emph{weight assignment}). We say that ${\cal G}$ is unambiguous if the underlying CFG is unambiguous.

The \emph{weight} of a derivation $d = \rho_1\ldots \rho_n$ is the element in $K$ defined by
\[
\wt(d) = \Val( \wt(\rho_1), \ldots, \wt(\rho_n))\enspace.
\]

We say that $\G$ is a \emph{weighted context-free grammar} (WCFG) if
$D(w)$ is  finite for every $w \in \Sigma^*$ or if $K$ is complete. In this case we define the  \emph{quantitative language} of $\G$ to be the series $\beh \G \beh \in K\fl \Sigma^*\fr$ given for every $w \in \Sigma^*$ by
\[
(\beh \G \beh,w)  = \sum_{d \in D(w)} \wt(d)\enspace.
\]
Note that this sum exists by our assumptions on a WCFG.
A series $s  \in K\fl \Sigma^*\fr$ is a \emph{quantitative
  context-free language} if there is a WCFG $\G$ such that $s = \beh
\G \beh$. The class of all quantitative context-free languages over
$\Sigma$ and  $K$ is denoted by $\CF(\Sigma,K)$. Moreover, we let
$\uCF(\Sigma,K)$ comprise all series $\beh \G \beh$ where $\G$ is an
unambiguous WCFG. We say that two WCFG are \emph{equivalent}, if they have the same quantitative language.

Clearly, any CFG $\G$ can be transformed into a WCFG over the Boolean
semiring $\mathbb{B}$ by adding the weight assignment $\wt: P
\rightarrow \mathbb{B}$ such that $\wt(\rho) = 1$ for each $\rho
\in P$. Then for each $w \in \Sigma^*$ we have $w \in L(\G)$ if and
only if $(\beh \G \beh,w) = 1$, i.e., $\beh \G\beh =
\one_{L(\G)}$.  Consequently, a language $L$ is context-free if and
only if $\one_L \in \CF(\Sigma,\mathbb{B})$.
 This shows that WCFG form a generalization of CFG.



We say that a CFG $\G=(N,\Sigma,Z,P,\wt)$ with weights is
{\em proper} if the right-hand side of each rule is an element of $(N
\cup \Sigma)^+ \setminus N$ (cf. \cite[p.302]{kuisal86}), i.e., $\G$ contains neither chain
productions $A\rightarrow B$ nor $\varepsilon$-productions $A\rightarrow \varepsilon$. Then obviously the set  $D(w)$ is finite for every $w \in
\Sigma^*$.

\begin{ob} A proper CFG with weights is a WCFG.
\end{ob}


A WCFG $\G$ is in \emph{head normal form} if every production has the form
\[
A \rightarrow xB_1\ldots B_k
\]
where $x \in \Sigma \cup \{\varepsilon\}$, $k \ge 0$,  and $A,B_1,\ldots,B_k \in N$.

\begin{lm}\label{lm:WCFG:normal-form} For every (unambiguous) WCFG there is an
  equivalent (unambiguous) WCFG in head normal form.
\end{lm}
\begin{proof} Let $\G = (N,\Sigma,Z,P,\wt)$ be a WCFG. We construct the CFG with weights $\G' = (N',\Sigma,Z,P',\wt')$ such that
\begin{itemize}
\item $N' = N \cup \{A_\sigma \mid \sigma \in \Sigma\}$,
\item $P'$ and $\wt'$ are determined as follows.
\begin{itemize}
\item If $A \rightarrow \varepsilon$ is in $P$, then $A \rightarrow \varepsilon$ is in $P'$; moreover, $\wt'(A \rightarrow \varepsilon) = \wt(A \rightarrow \varepsilon)$.

\item If $A \rightarrow X\xi$ in $P$ with $X \in N\cup \Sigma$ and $\xi \in (N\cup \Sigma)^*$, then $A \rightarrow X\xi'$ is  in $P'$ where $\xi'$ is obtained from $\xi$ by replacing every $\sigma \in \Sigma$ by $A_\sigma$; moreover, $\wt'(A \rightarrow X\xi') = \wt(A \rightarrow X\xi)$.

\item For every $\sigma \in \Sigma$, the production $A_\sigma \rightarrow \sigma$ is in $P'$; moreover, $\wt'(A_\sigma \rightarrow \sigma) = 1$.
\end{itemize}
\end{itemize}
Then, for every $w \in \Sigma^*$, we have that  every derivation $d$ of $w$ by $\G$ corresponds naturally to a uniquely determined derivation of $w$ by  $\G'$, and vice versa.  Thus $\G'$ is also a WCFG and corresponding successful derivations have the same weight. Thus $\beh \G \beh = \beh \G'\beh$.  Clearly, $\G$ is unambiguous if and only if $\G'$ is unambiguous.
\end{proof}


\eat{
\begin{lm}\label{lm:A-finite} For every WCFG $\G = (N,\Sigma,Z,P,\wt)$
  there is an equivalent WCFG $\G' = (N,\Sigma,Z,P',\wt')$ such that
  $P' \subseteq P$, $\wt' = \wt|_{P'}$, and for every $A \in N$ and $w
  \in \Sigma^*$ the set $D_{\G'}(A,w)$ is finite. If $\G$ is in head normal form, then so is $\G'$.
\end{lm}
\begin{proof} We define the set $N' = \{B \in N \mid \exists u\in
  \Sigma^*: D_\G(B,u) \text{ is not finite}\}$.
 Then we let $P'$   contain each production $\rho \in P$ such that every nonterminal in its right-hand side is an element of  $N\setminus N'$.

Let $w \in \Sigma^*$. Clearly, $D_{\G'}(w) \subseteq D_\G(w)$. Now let $d = \rho_1 \ldots \rho_n \in D_\G(w)$. Then $d$ cannot contain a production with a nonterminal in $N'$. On the contrary, assume that there is an $1 \le i \le n$ such that the left hand side of $\rho_i$ is  $B \in N'$. Then, by Observation \ref{ob:dec}, there are uniquely determined (i) $j$ with $i+1 \le j \le n$ and (ii)  $v_1,w',v_2 \in \Sigma^*$, such that
\begin{compactitem}
\item $w = v_1w'v_2$,
\item $d = \rho_1 \ldots \rho_i \ldots \rho_j \ldots \rho_n$, and
\item $\rho_i\ldots \rho_j \in D_\G(B,w')$.
\end{compactitem}
Since $B \in N'$, there is a $u\in\Sigma^*$ such that $D_\G(B,u)$ is not finite. Since
\[
\{\rho_1 \ldots \rho_{i-1} d \rho_{j+1} \ldots \rho_n \mid d \in D_\G(B,u)\} \subseteq D_\G(v_1uv_2)\enspace,
\]
we obtain that $D_\G(v_1uv_2)$ is not finite. This contradicts the fact that $\G$ is a WCFG. Hence $d \in D_{G'}(w)$.

Thus $D_{\G'}(w) = D_\G(w)$ for every $w \in \Sigma^*$, and $\beh \G\beh = \beh \G'\beh$.
\end{proof}

}%

\begin{ex}\rm \label{ex:wcfg} We consider the set of all arithmetic expressions over   addition, multiplication, and the variable $x$. Assuming that the calculation  of the addition (and multiplication) of two values needs $n \in
  \mathbb{N}$ (resp., $m \in \mathbb{N}$) machine  clock cycles, we might wish to know the average number of clock cycles it  needs to calculate any of the operations occuring in an expression.

For this we consider the unital valuation monoid $(\mathbb{R} \cup \{-\infty, \infty\}, \sup, \mathrm{avg}, -\infty, \infty)$ as in Example \ref{ex:val}(2) and the WCFG $\G = (N,\Sigma,E,P)$ with the following  set of productions and  associated values:
\[
\begin{array}{lrcllrcl}
\rho_1: & E & \stackrel{n}{\rightarrow} & E + E \hspace{5mm}
&  \rho_2: & E & \stackrel{m}{\rightarrow} & E * E \\
\rho_3: &E & \stackrel{1}{\rightarrow} & ( E ) &  \rho_4: &E & \stackrel{1}{\rightarrow} & x  \enspace.
\end{array}
\]
For the expression $w = x * x + x* x$, the set of derivations is $D(w) = \{d\}$ with $d = \rho_1 d' d'$ and  $d' = \rho_2 \rho_4 \rho_4$. In fact, $\G$ is unambiguous.
 Then
\[
(\beh {\cal G} \beh, w) = \wt(d) = \Val(n, \underbrace{m,1,1,}_{d'} \, \underbrace{m,1,1}_{d'}) = \mathrm{avg}(n,m,m) = \frac{n + 2\cdot m}{3}\enspace.
\]
\end{ex}

%
\section{Weighted Pushdown Automata}


In this section, we introduce our notion of weighted pushdown automata, and we derive a few basic properties. First let us fix our notation for pushdown automata. Let $\Sigma$ be an alphabet. A \emph{pushdown automaton} (PDA) over $\Sigma$ is a tuple $\M = (Q,\Gamma,q_0,\gamma_0,F,T)$ where
$Q$ is a finite set (\emph{states}),
 $\Gamma$ is an alphabet (\emph{pushdown symbols}),
$q_0 \in Q$ (\emph{initial state}),
$\gamma_0 \in \Gamma$ (\emph{initial pushdown symbol}),
 $F \subseteq Q$ (\emph{final states}), and
\[T \subseteq_{f} Q \times \big(\Sigma \cup \{\varepsilon\}\big) \times \Gamma \times Q \times \Gamma^*,
\] a finite set (\emph{transitions}).
Let $(q,x,\gamma,p,\pi)$ be a transition. We call $q$, $x$, and $p$ its \emph{source state}, \emph{label}, and \emph{target state}, respectively.
%


The computation relation of $\M$ is the binary relation on the set $Q \times \Sigma^* \times \Gamma^*$ of \emph{configurations} defined as follows. For every transition $\tau = (q,x,\gamma,p,\pi) \in T$ we define
the binary relation
\[
\stackrel{\tau}{\vdash} \; \; \subseteq \; \; (Q \times \Sigma^* \times \Gamma^*) \times  (Q \times \Sigma^* \times \Gamma^*)
\]
such that for every $w \in \Sigma^*$ and $\mu \in \Gamma^*$, we have
\[
(q,xw,\gamma\mu) \stackrel{\tau}{\vdash} (p,w,\pi\mu)\enspace.
\]
The \emph{computation relation of $\M$} is the binary relation $\vdash\ = \bigcup_{\tau \in T} \stackrel{\tau}{\vdash}$.

A \emph{computation} is a sequence $\theta = \tau_1 \ldots \tau_n$ of transitions $\tau_i$ such that there are configurations $c_0,\ldots,c_n$ with  $c_{i-1} \stackrel{\tau_i}{\vdash} c_{i}$ for every $1 \le i \le n$. We abbreviate this computation by $c_0 \stackrel{\theta}{\vdash} c_n$.
The \emph{label} of a computation  $\tau_1 \ldots \tau_n$ is the
sequence of labels of the involved transitions. Let $w \in \Sigma^*$
and $q \in Q$. A \emph{$q$-computation on $w$} is a
computation $\theta$ such that $(q,w,\gamma_0)
\stackrel{\theta}{\vdash} (p,\varepsilon,\varepsilon)$ for some $p \in
F$. We let $\Theta(q,w)$ denote the set of all $q$-computations on $w$, and we let $\Theta(w) =\Theta(q_0,w)$. Moreover, we let $\Theta = \bigcup_{w \in \Sigma^*}\Theta(w)$.

The \emph{language recognized by $\M$} is the set
\[
L(\M) = \{ w \in \Sigma^* \mid \Theta(w) \not= \emptyset\}\enspace.
\]
That means, we consider acceptance of words by final state and empty pushdown.



\begin{ob}\label{obs:decomp-PDA}
Let $(q,v,\gamma_1 \ldots \gamma_k) \stackrel{\eta}{\vdash} (p,\varepsilon,\varepsilon)$ be a computation. Put $p_0 = q$. Then for $i=1,\ldots, k$ we obtain successively a uniquely determined shortest computation $\eta_i$, state $p_i\in Q$, and word $v_i\in\Sigma^*$ such that $(p_{i-1},v_i,\gamma_i) \stackrel{\eta_i}{\vdash}(p_i,\varepsilon,\varepsilon)$ and $\eta = \eta_1 \ldots \eta_k$,
 $v = v_1 \ldots v_k$,
 and $p_k = p$.
\end{ob}

Let $\M$ be any PDA. We say that $\M$ is {\em ambiguous} if there is a $w \in L(\M)$ such that $|\Theta(w)| \ge 2$; otherwise $\M$ is {\em unambiguous}.



Next let $K$ be a unital valuation monoid. A \emph{pushdown automaton with weights in $K$} is a tuple $\M = (Q,\Gamma,q_0,\gamma_0,F,T,\wt)$ where
$(Q,\Gamma,q_0,\gamma_0,F,T)$ is a PDA and  $\wt: T \rightarrow K$ is a mapping (\emph{weight assignment}). We say that ${\cal M}$ is unambiguous if the underlying PDA is unambiguous.


The \emph{weight} of a computation $\theta = \tau_1 \ldots \tau_n$ is the element in $K$ defined by
\[
\wt(\theta) = \Val( \wt(\tau_1), \ldots, \wt(\tau_n))\enspace.
\]

We say that $\M$ is a \emph{weighted pushdown automaton} (WPDA) if
$\Theta(w)$ is finite for every $w \in \Sigma^*$ or if $K$ is complete.
 In this case we define the \emph{quantitative behavior} of $\M$ to be the series $\beh \M \beh \in K\fl \Sigma^* \fr$ given for every $w \in \Sigma^*$ by
\[
(\beh \M\beh, w) = \sum_{\theta \in \Theta(w)} \wt(\theta)\enspace.
\]
The class of  quantitative behaviors of all WPDA over $\Sigma$ and  $K$ is denoted by $\PDA(\Sigma,K)$.  Moreover, we let
$\uPDA(\Sigma,K)$ comprise all series $\beh \M \beh$ where $\M$ is an
unambiguous WPDA. We say that two WPDA are \emph{equivalent}, if they have the same quantitative behavior.


Clearly, any PDA $\M$ can be transformed into a WPDA over the Boolean
semiring $\mathbb{B}$ by adding the weight assignment $\wt: T
\rightarrow \mathbb{B}$ such that $\wt(\tau) = 1$ for each $\tau
\in T$. Then for each $w \in \Sigma^*$ we have $w \in L(\M)$ if and
only if $(\beh \M \beh,w) = 1$, i.e., $\beh \M\beh =
\one_{L(\M)}$.  Consequently, a language $L$ is recognized by a PDA if and
only if $\one_L \in \PDA(\Sigma,\mathbb{B})$. This shows that WPDA form a generalization of PDA.






We say that a PDA $\M
=(Q,\Gamma,q_0,\gamma_0,F,T,\wt)$ with weights is {\em proper} if
$(q,\varepsilon,\gamma,p,\pi) \in T$ implies $|\pi| \ge 2$ (cf. \cite[p.172]{kuisal86}), i.e., $\M$ extends its pushdown in each
$\varepsilon$-transition. Then obviously the set  $\Theta(w)$ is finite for every $w
\in \Sigma^*$.

\begin{ob} Each proper PDA with weights is a WPDA.
\end{ob}


A WPDA  $\M = (Q,\Gamma,q_0,\gamma_0,F,T,\wt)$ is \emph{state
  normalized} if
\begin{itemize}
\item there is no transition in $T$ with $q_0$ as target state,
\item $F$ is a singleton, say, $F = \{q_f\}$, and
\item there is no transition in $T$ with $q_f$ as source state.
\end{itemize}

\begin{lm}\label{lm:WPDA-normalized} For every (unambiguous) WPDA there is an
  equivalent state normalized (unambiguous)  WPDA.
\end{lm}
\begin{proof} \sloppy Let $\M = (Q,\Gamma,q_0,\gamma_0,F,T,\wt)$. We construct
  the PDA with weights $\M' = (Q',\Gamma',q_0',\gamma_0',\{q_f\},T',\wt')$ with
\begin{itemize}
\item $Q' = Q \cup \{q_0',q_f\}$ with $Q \cap \{q_0',q_f\} = \emptyset$,
\item $\Gamma' = \Gamma \cup \{\gamma_0'\}$,
\item $T' = T \cup
  \{\tau_{\mathrm{in}}\} \cup
  \{\tau_p \mid p \in F \}$,  $\tau_{\mathrm{in}} = (q_0',\varepsilon,\gamma_0',q_0,\gamma_0\gamma_0')$ and $\tau_p = (p,\varepsilon,\gamma_0',q_f,\varepsilon)$
  and
\item $\wt'|_T = \wt$ and
  $\wt'(\tau_{\mathrm{in}}) =
  \wt(\tau_p) = 1$, for each $p\in F$.
\end{itemize}
\sloppy Let $\theta = \tau_1 \tau_2 \ldots \tau_n$ be a computation of $\M$ on $w$ and let $p$ be the target state of $\tau_n$. Then $\theta' =
\tau_{\mathrm{in}} \tau_1 \tau_2 \ldots \tau_n \tau_p$ is a computation of $\M'$ on $w$ and $\wt'(\theta') = \wt(\theta)$. Vice versa, every computation of $\M'$ on $w$ has the form $\tau_{\mathrm{in}} \tau_1 \tau_2 \ldots \tau_n \tau_p$ for some $p \in F$. Then $\tau_1 \tau_2 \ldots \tau_n$ is a computation of $\M$ on $w$.

Moreover,  $\M'$ is a WPDA. Thus we have $\beh \M\beh = \beh \M'\beh$. Clearly,  $\M$ is unambiguous if and only if $\M'$ is unambiguous.
\end{proof}


Next we show that WPDA with just one state are as powerful as
arbitrary WPA using the classical triple construction (cf. e.g. \cite[Lecture 25]{koz97}).

\begin{lm}\label{lm:WPDA-one-state} For every (unambiguous) WPDA there is an equivalent (unambiguous) WPDA with just one state.
\end{lm}
\begin{proof}\sloppy Let $\M$ be a WPDA. By Lemma
  \ref{lm:WPDA-normalized} we can assume that $\mathcal{M}$ is state normalized and has the form $(Q,\Gamma,q_0,\gamma_0,\{q_f\},T,\wt)$. Then we construct the PDA with weights $\M' = (\{\ast\},\Gamma',\ast, (q_0,\gamma_0,q_f), \{\ast\},T',\wt')$ and $\Gamma' = Q \times \Gamma \times Q$ as follows. For each transition
\[(q,x,\gamma,p_0,\gamma_1\ldots \gamma_k) \in T
\]
and every $p_1,\ldots,p_k \in Q$, the transition
\[
(\ast,x,(q,\gamma,p_k),\ast,(p_0,\gamma_1,p_1)(p_1,\gamma_2,p_2)\ldots (p_{k-1},\gamma_k,p_k))
\]
is in $T'$. For $k=0$ this reads: if $(q,x,\gamma,p_0,\varepsilon) \in T$, then $(\ast,x,(q,\gamma,p_0),\ast,\varepsilon) \in T'$.

Moreover,
\[\wt'((\ast,x,(q,\gamma,p_k),\ast,(p_0,\gamma_1,p_1)(p_1,\gamma_2,p_2)\ldots (p_{k-1},\gamma_k,p_k))) = \wt((q,x,\gamma,p_0,\gamma_1\ldots \gamma_k)))\enspace.
\]

For every computation $\theta$ of ${\cal M}$ we construct a
computation  $\varphi(\theta)$ of $\M'$ as follows. Let $\theta \in
\Theta_\M(w)$ and $\tau = (q,x,\gamma,p,\gamma_1\ldots \gamma_k)$ be a transition which occurs in $\theta$. Then
$\theta$ can be decomposed into
\[
(q_0,w,\gamma_0)
\stackrel{\theta_1}{\vdash} (q,xu,\gamma\mu)
\stackrel{\tau}{\vdash} (p,u,\gamma_1\ldots \gamma_k\mu)
\stackrel{\theta_2}{\vdash} (q_f,\varepsilon,\varepsilon) \enspace.
\]
Let $\eta$, $v$, and $p'$ be the, resp., shortest prefix of
$\theta_2$, shortest prefix of $u$, and uniquely determined state such that
\[
(p,v,\gamma_1\ldots \gamma_k) \stackrel{\eta}{\vdash} (p',\varepsilon,\varepsilon)\enspace.
\]
Put $p_0=p$. Then, by Observation \ref{obs:decomp-PDA}, for $i=1,\ldots,k$ we can successively find a shortest word $v_i \in \Sigma^*$, a uniquely determined state $p_i \in Q$, and a shortest computation $\eta_i$ such that $(p_{i-1},v_i,\gamma_i) \stackrel{\eta_i}{\vdash} (p_i,\varepsilon,\varepsilon)$ and  $v = v_1 \ldots v_k$, $p_k=p'$, and $\eta = \eta_1\ldots \eta_k$.
Then we replace the occurrence $\tau$ in $\theta = \theta_1 \tau \theta_2$ by
\[
\varphi(\tau) = (\ast,x,(q,\gamma,p_k),\ast,(p,\gamma_1,p_1)(p_1,\gamma_2,p_2)\ldots (p_{k-1},\gamma_k,p'))\enspace.
\]
We extend $\varphi$ to computations by letting
\[
\varphi(\tau_1\ldots \tau_n) = \varphi(\tau_1) \ldots \varphi(\tau_n)\enspace.
\]
In particular, $\varphi: \Theta_\M(w) \rightarrow \Theta_{\M'}(w)$ is
bijective. Thus, since $\M$ is a WPDA, also $\M'$ is a WPDA.
Since $\wt(\tau) = \wt(\varphi(\tau))$, we have $\wt(\theta) =
\wt(\varphi(\theta))$. Hence, $\beh \M \beh = \beh \M'\beh$.

It is clear that $\M$ is unambiguous if and only if $\M'$ is unambiguous.
\end{proof}




\begin{lm}\label{lm:WPDA-sum} Let $s_1,s_2 \in \PDA(\Sigma,K)$. Then $s_1 + s_2 \in \PDA(\Sigma,K)$.
\end{lm}
\begin{proof} Let $\M_1 = (Q_1,\Gamma_1,q_{0,1},\gamma_{0,1},F_1,T_1,\wt_1)$ and
$\M_2 = (Q_2,\Gamma_2,q_{0,2},\gamma_{0,2},F_2,T_2,\wt_2)$ be state normalized WPDA such that $s_1 = \beh \M_1\beh$ and $s_2 = \beh \M_2\beh$. Without loss of generality we can assume that
\begin{compactitem}
\item $q_{0,1}= q_{0,2}$ and $Q_1 \cap Q_2 = \{q_{0,1}\}$; henceforth we will denote this initial state by $q_0$, and
\item  $\gamma_{0,1} = \gamma_{0,2}$; henceforth we will denote this initial pushdown symbol by $\gamma_0$.
\end{compactitem}
%
%
%


Now we construct the WPDA $\M = (Q,\Gamma,q_0,\gamma_0,F,T,\wt)$ with
$Q = Q_1 \cup Q_2$, $\Gamma = \Gamma_1 \cup \Gamma_2$, $F = F_1 \cup
F_2$, and $T = T_1 \cup T_2$. Moreover, we let $\wt|_{T_1} = \wt_1$
and  $\wt|_{T_2} = \wt_2$. Then $\beh \M \beh = \beh \M_1\beh + \beh \M_2\beh$.
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\end{proof}

Finally, we mention that in \cite{chavel12} pushdown games with quantitative objectives were investigated.
Such games are formalized on the basis of paths through pushdown systems where the latter are particular pushdown automata with weights: the input alphabet $\Sigma$ is a singleton and no $\varepsilon$-transition occurs.
Moreover, as weight structure, pushdown systems employ the set of integers with mean-payoff.
Roughly, the mean-payoff of a computation is the average of its transition weights (taking the limes superior of the averages of finite prefixes on infinite computations).
Then in \cite{chavel12} game-theoretic problems on the set of all paths for which the mean-payoff is above a given threshold are investigated.


%
\section{Equivalence of WCFG and WPDA}

A classical result says that a language $L$ is context-free if, and
only if $L$  is accepted by a pushdown automaton. This was extended to algebraic series and weighted
pushdown automata with weights taken in semirings in
\cite[Cor. 14.16]{kuisal86}. The goal of this  section is to prove the following generalization to arbitrary unital valuation monoids.

\begin{theo}\label{th:PDA=CF} For every alphabet $\Sigma$ and
  unital valuation monoid $K$ we have $\PDA(\Sigma,K) =
  \CF(\Sigma,K)$ and $\uPDA(\Sigma,K) =
  \uCF(\Sigma,K)$.
\end{theo}


We will prove this theorem by showing that WCFG in head normal form and WPDA with one state are equivalent models (cf. e.g. \cite[Lecture 25]{koz97}).

Let $\M = (\{\ast\},\Gamma,\ast,\gamma_0,\{\ast\},T,\wt_{\M})$ be a WPDA over $\Sigma$ and $K$ with one state and $\G = (N,\Sigma,Z,P,\wt_{\G})$ be a WCFG over $K$ in head normal form. We say that $\M$ and $\G$ are \emph{related} if
\begin{itemize}
\item $\Gamma = N$,
\item $\gamma_0 = Z$,
\item $\tau = (\ast,x,A,\ast,B_1B_2\ldots B_n) \in T$ iff
$\rho = (A \rightarrow xB_1B_2\ldots B_n)$ is in $P$.
\item $\wt_{\M}(\tau) = \wt_{\G}(\rho)$ if $\tau$ and $\rho$ correspond to each other as above.
\end{itemize}

\begin{lm}\label{lm:related} Let $\M$ be a WPDA with one state  and $\G$ be a WCFG in head normal form. If $\M$ and $\G$ are related, then $\beh \M \beh = \beh \G\beh$. Moreover, $\M$ is unambiguous if and only if $\G$ is unambiguous.
\end{lm}

\begin{proof} For every $w \in \Sigma^*$, the set $\Theta(w)$ of computations on $w$ corresponds bijectively to the set $D(w)$ of derivations of $w$, and this correspondence preserves their weights. This implies $(\beh \M \beh,w) = (\beh \G\beh,w)$.
\end{proof}


\emph{Proof of Theorem \ref{th:PDA=CF}}: If $s \in \PDA(\Sigma,K)$, then
by Lemma \ref{lm:WPDA-one-state} there is a WPDA ${\cal M}$ with one state such that $\beh {\cal M}\beh =s$. Next we construct the WCFG ${\cal G}$ which is related to ${\cal M}$. By Lemma \ref{lm:related} we obtain that $s \in \CF(\Sigma,K)$. Correspondingly, the converse follows from Lemmas \ref{lm:WCFG:normal-form} and \ref{lm:related}.
\hfill $\Box$


%
\section{Theorem of Chomsky-Sch\"utzenberger}
\label{sec:Chomsky-Sch}

In this section let $K$ again be a unital valuation monoid. The
goal of this section will be to prove a quantitative version of the
Chomsky-Sch\"utzenberger theorem.

Let $Y$ be an alphabet. Then we let $\overline{Y} = \{\overline{y}
\mid y \in Y\}$. The \emph{Dyck-language over $Y$}, denoted by $\D_Y$,
is the language which is generated by the CFG $\G_Y =
(N,Y \cup \overline{Y}, Z,P)$ with $N = \{Z\}$ and the rules $Z
\rightarrow y Z \overline{y}$, $Z \rightarrow ZZ$, and $Z \rightarrow
\varepsilon$.

Next we introduce the concept of alphabetic morphism.
A series $s \in K\fl \Sigma^*\fr$  is called a \emph{monome} if $\supp(s)$ is empty or a singleton.
If $\supp(s) = \{w\}$, then we also write $s = (s,w).w$\enspace.
We let $K\langle \Sigma \cup \{\varepsilon\}\rangle$ denote the set of all monomes with support in $\Sigma \cup \{\varepsilon\}$.

Let $\Delta$ be an alphabet and $h: \Delta \rightarrow K\langle\Sigma
\cup \{\varepsilon\}\rangle$ be a mapping. The  \emph{alphabetic morphism induced by $h$} is the mapping $h': \Delta^* \rightarrow  K\fl \Sigma^*\fr$ such that for every $n \ge 0$, $\delta_1,\ldots,\delta_n \in \Delta$ with $h(\delta_i) = a_i . y_i$ we have
\[
h'(\delta_1 \ldots \delta_n) = \Val(a_1,\ldots,a_n).y_1\ldots y_n\enspace.
\]
Note that $h'(v)$ is a monome for every $v \in \Delta^*$, and $h'(\varepsilon) = 1.\varepsilon$.
If $L \subseteq \Delta^*$ such that the family $(h'(v) \mid v \in L)$
is locally finite or if $K$ is complete, we let $h'(L) = \sum_{v\in L} h'(v)$. In the sequel we identify $h'$ and $h$.

Our main result will be:

\begin{theo}\label{th:char} Let $K$ be a unital valuation monoid and  $s \in K\fl \Sigma^*\fr$ be a series. Then the following three statements are equivalent.
\begin{enumerate}
\item $s \in \CF(\Sigma,K)$.
\item There are
  an alphabet $Y$, a recognizable language $R$ over
  $Y\cup\overline{Y}$, and an alphabetic morphism $h: Y \cup \overline{Y}
  \rightarrow K\langle\Sigma \cup \{\varepsilon\}\rangle$ such that $s = h(\D_Y \cap R)$.
\item There are an alphabet $\Delta$, an unambiguous CFG $\G$ over
  $\Delta$, and an alphabetic morphism $h: \Delta \rightarrow
  K\langle\Sigma \cup \{\varepsilon\}\rangle$ such that $s = h(L(\G))$.
\end{enumerate}
Moreover, if $K$ is complete and completely idempotent, then 1-3
%
are also
equivalent to:
\begin{enumerate}
\item[4.] There are an alphabet $\Delta$, a context-free language $L$
  over $\Delta$, and an alphabetic morphism $h: \Delta \rightarrow
  K\langle\Sigma \cup \{\varepsilon\}\rangle$ such that $s = h(L)$.
\end{enumerate}
\end{theo}

First we investigate alphabetic morphisms.

\begin{lm}\label{th:mezwri}  Let $s \in \CF(\Sigma,K)$. Then there are
  an alphabet $\Delta$, an unambiguous CFG $\G$ over $\Delta$, and an
  alphabetic morphism $h: \Delta \rightarrow K\langle\Sigma \cup
  \{\varepsilon\}\rangle$ such that
%
%
$s = h(L(\G))$.
\end{lm}

\begin{proof} By Lemma \ref{lm:WCFG:normal-form} we can assume that $s = \beh \HH \beh$ for some WCFG $\HH = (N,\Sigma,Z,P,\wt)$ in head normal form.

We let $\Delta = P$, and we construct the CFG $\G = (N,P,Z,P')$ and the mapping $h:
P \rightarrow K\langle\Sigma \cup \{\varepsilon\}\rangle$ such
that, if $\rho = (A \rightarrow x B_1\ldots B_k)$ is in $P$, then $A
\rightarrow \rho B_1 \ldots B_k$ is in $P'$ and we define $h(\rho) =
\wt(\rho).x$. Obviously, $\G$ is unambiguous.

By definition of $h$, we have that $h(d) =
\Val(\wt(\rho_1),\ldots,\wt(\rho_n)).w$ for every $w \in \Sigma^*$ and $d = \rho_1\ldots
\rho_n\in D_{\cal H}(w)$. Hence $\wt(d) = (h(d),w)$.

It is clear that $L(\G) = \bigcup_{w \in \Sigma^*} D_{\cal H}(w)$ and $D_{\cal H}(w) \cap D_{\cal H}(w') = \emptyset$ for every $w \not= w'$.
 Hence, $\{d \in L(\G) \mid (h(d),w) \not= 0\} \subseteq D_{\cal H}(w)$,
which is finite by definition of WCFG in case $K$ is not complete. Thus, $(h(d) \mid d
\in L(\G))$ is locally finite if  $K$ is not complete.


Then for every $w \in \Sigma^*$ we have
\[
\begin{array}{l}
(\beh \HH\beh, w) = \sum_{d \in D_{\HH}(w)} \wt(d) = \sum_{d \in D_{\HH}(w)}
(h(d),w)\\
 =^*  \sum_{d \in L(\G)} (h(d),w) = \left(  \sum_{d \in L(\G)}
  h(d) , \; w \right) = (h(L(\G)),w)
\end{array}
\]
where the equation $*$ holds, because for every $d \in L({\cal G}) \setminus D_{\cal H}(w)$ we have $(h(d),w) = 0$. Thus $s = h(L(\G))$.
\end{proof}

\begin{ex}\rm We apply the construction in the proof of Lemma \ref{th:mezwri} to the WCFG of Example \ref{ex:wcfg} and assume that it is given as the following WCFG $\cal{H}$ in head normal form:
\[
\begin{array}{lrcllrcl}
\rho_1: & E & \stackrel{n}{\rightarrow} & E \oplus E \hspace{5mm}
&  \rho_2: & E & \stackrel{m}{\rightarrow} & E \odot E \\
\rho_3: &E & \stackrel{1}{\rightarrow} & ( E \oslash &  \rho_4: &E & \stackrel{1}{\rightarrow} & x  \enspace.
\end{array}
\]
with the following three additional productions:
\[
\rho_5: \; \oplus  \stackrel{1}{\rightarrow}  +  \enspace, \hspace{10mm}
\rho_6: \; \odot   \stackrel{1}{\rightarrow}  * \enspace, \hspace{10mm}
\rho_7: \; \oslash  \stackrel{1}{\rightarrow} \; ) \enspace.
\]
In $\cal H$, the terminal string $w = x*x + x*x$ has the derivation $d = \rho_1d'\rho_5d'$ with
\[
d' = \rho_2 \rho_4 \rho_6 \rho_4\enspace.
\]
The application of the construction yields the CFG $\G$:
\[
\begin{array}{rclrclrcl}
E & \rightarrow & \rho_1 \, E \oplus E \hspace{5mm}&
E & \rightarrow & \rho_2 \, E \odot E \\
E & \rightarrow & \rho_3 \, E \oslash &
E & \rightarrow & \rho_4\\
\oplus & \rightarrow &  \rho_5 &
\odot  & \rightarrow &  \rho_6 &
\oslash & \rightarrow \rho_7
\end{array}
\]
and the alphabetic morphism $h$:
\[
\begin{array}{rclrclrcl}
h(\rho_1) & = & n.\varepsilon \hspace{5mm} &
h(\rho_2) & = & m.\varepsilon \\
h(\rho_3) & = &  1.( &
h(\rho_4) & = & 1.x \\
h(\rho_5) & = & 1.+  &
h(\rho_6) & = & 1.* \hspace{5mm}&
h(\rho_7) & = & 1.) \enspace.
\end{array}
\]
Then, using the abbreviation $d' = \rho_2 \rho_4 \rho_6 \rho_4$ and $w =   x*x + x*x$ as above, we have
\[
\begin{array}{rcl}
h(\rho_1d'\rho_5d') & = &
\Val(\underbrace{n}_{\rho_1}, \underbrace{m, 1, 1, 1}_{d'} \,\underbrace{1}_{\rho_5}, \underbrace{m,1,1,1}_{d'}) \, . \, w\\
& = & \mathrm{avg}(n,m,m)\, . \, w\\[4mm]
& = &  \frac{n + 2\cdot m}{3} \, . \, w\enspace,
\end{array}
\]
and hence $\wt(w) = (h(d),w)$.
\end{ex}


In the next lemma we show the converse of Lemma \ref{th:mezwri}.

\begin{lm}\label{lm:closure} Let $L$ be a context-free language over
  $\Delta$ and $h: \Delta \rightarrow K\langle\Sigma \cup
  \{\varepsilon\}\rangle$ an alphabetic morphism such that $(h(v) \mid
  v \in L)$ is locally finite in case $K$ is not complete. If $L$ can be generated by some
  unambiguous CFG or if  $K$ is complete and completely idempotent, then $h(L) \in \CF(\Sigma,K)$.
\end{lm}
\begin{proof} Let $\M =(Q,\Gamma,q_0,\gamma_0,F,T)$ be a PDA over
  $\Delta$ with $L(\M) =L$. Moreover, by Theorem \ref{th:PDA=CF}, if
  $L = L(\G)$ for some unambiguous CFG $\G$, then we can assume that $\M$ is unambiguous.
 Let $\overline{\delta} \in \Delta$ be an arbitrary, but fixed element.

\sloppy  The following construction employs the same technique as in
\cite[Lemma 5.7]{drovog12} of coding the preimage of $h$ into the state
set; thereby non-injectivity of $h$ is handled appropriately. We construct the PDA over $\Sigma$ with weights $\M' =
(Q',\Gamma,q_0',\gamma_0,F',T',\wt)$ where $Q' = \{q_0'\} \cup  Q \times
(\Delta \cup \{\varepsilon\})$ for some $q_0' \not\in Q$, $F' = F\times \{\overline{\delta}\}$, and $T'$ and $\wt$ are defined as follows.

\begin{itemize}
\item For every $x \in \Delta \cup \{\varepsilon\}$, the rule $\tau =
  (q_0',\varepsilon,\gamma_0,(q_0,x),\gamma_0)$ is in $T'$ and
  $\wt(\tau) =1$.


\item Let $\tau = (q,x,\gamma,p,\pi) \in T$ and $x' \in \Delta\cup
\{\varepsilon\}$.
\begin{itemize}
\item If $x \in \Delta$ and $h(x) = a.y$, then $\tau' =
  ((q,x),y,\gamma,(p,x'),\pi) \in T'$  and $\wt(\tau') = a$.

\item If $x = \varepsilon$, then $\tau' =
  ((q,\varepsilon),\varepsilon,\gamma,(p,x'),\pi) \in T'$ and
  $\wt(\tau') = 1$.
\end{itemize}
\end{itemize}


Let $v = \delta_1 \ldots \delta_n \in \Delta^*$ with  $n\ge 0$ and
$\delta_i \in \Delta$.  Let $h(\delta_i) = a_i.y_i$ for every
$1 \le i \le n$. Thus $h(v) = \Val(a_1,\ldots,a_n). y_1\ldots y_n$.


 Let $\theta = \tau_1 \ldots \tau_m$ be
a $q_0$-computation in $\Theta_{\M}(v)$; note that $m \ge
\max\{n,1\}$ because at least $\gamma_0$ has to be popped. Let $x_i$ be the second component of $\tau_i$, so, $x_i \in \Delta \cup \{\varepsilon\}$.

Then we construct the  $q_0'$-computation
$\theta' = \tau_0'\tau_1'\ldots \tau_m'$ in
$\Theta_{\M'}(y_1\ldots y_n)$  as follows:
\begin{itemize}
\item $\tau_0' = (q_0',\varepsilon,\gamma_0,(q_0,x_1),\gamma_0)$.

\item If $1 \le i \le m$ and  $\tau_i = (q,x_i,\gamma,p,\pi)$, then $\tau_i' =
  ((q,x_i),y',\gamma,(p,x_{i+1}),\pi)$ where $y' = y$ if $x_i \in \Delta$ and
  $h(x_i) = a.y$, and $y' = \varepsilon$ if $x_i = \varepsilon$, and $x_{m+1}=\overline{\delta}$.

%
%
%
 \end{itemize}

Note that if $x_i \in \Delta$ and $h(x_i) = a.y$, then $\wt(\tau_i') =
a$, and if $x_i = \varepsilon$, then $\wt(\tau_i') = 1$ for each $1
\le i \le m$, by definition of $\wt$. Consequently, if $w \in
\Sigma^*$ and $(h(v),w) \not= 0$, then $w = y_1\ldots y_n$ and
\[
(h(v),w) = \Val(a_1,\ldots,a_n) =
\Val(\wt(\tau_0'),\wt(\tau_1'),\ldots,\wt(\tau_m')) = \wt(\theta').
\]



Conversely, for every  $q_0'$-computation $\theta' =
\tau_0'\tau_1'\ldots \tau_m'$ in $\Theta_{\M'}(y_1\ldots y_n)$ there
is a uniquely determined  $q_0$-computation $\theta = \tau_1
\ldots \tau_m$ in $\Theta_{\M}(v)$ such that $\theta'$ is the
computation constructed above. It follows that $\M'$ is a WPDA.

In particular, if $(h(v),w) \not= 0$, then $\wt(\theta_1') = (h(v),w)
= \wt(\theta_2')$ for every $\theta_1',\theta_2' \in \Theta_{\M}(v)$.

So, for every $w \in \Sigma^*$ we obtain
\[
\begin{array}{ll}
  & (h(L(\M)),w) \; = \; \left( \sum_{v \in L(\M)} h(v), \, w\right)\\[3mm]
=   & \sum_{\substack{v \in L(\M):\\(h(v),w) \not=0}} (h(v), w)\\[5mm]
=^*   & \sum_{\substack{\theta \in \Theta_{\M}(v):\\(h(v),w) \not=0}} (h(v), w)\\[5mm]
= & \sum_{\theta' \in \Theta_{\M'}(w)} \wt(\theta')\\[3mm]
= & (\beh \M'\beh, w)
\end{array}
\]
where the $*$-marked equality holds because (1) $K$ is complete and
completely idempotent or (2) $\M$ is unambiguous.
Thus $\beh \M' \beh = h(L(\M))$ and the result follows from Theorem \ref{th:PDA=CF}.
\end{proof}

We include the argument for the following simple observation for the sake of completeness.

\begin{ob}\label{ob:Dyck} $\ $
\begin{enumerate}
\item There is an unambiguous CFG $\G$ such that $L(\G) = \D_Y$.
\item Let $\G$ be an unambiguous CFG over $\Sigma$ and $R
  \subseteq \Sigma^*$ is a regular language. Then there is an
  unambiguous CFG $\G'$ with $L(\G') = L(\G) \cap R$.
\end{enumerate}
\end{ob}
\begin{proof} 1. We consider the CFG $\G_Y' =
(N,Y \cup \overline{Y}, Z,P)$ with $N = \{Z,A\}$ and the rules $Z
\rightarrow AZ$, $Z \rightarrow
\varepsilon$, and  $A\rightarrow y Z \overline{y}$. Clearly, $L(\G_Y')
= \D_Y$, and $\G_Y'$ is unambiguous (cf. \cite[Prop.1, p.145]{chosch63}).

2. Using \cite[Lm.4.1]{barpersha61} we can construct the CFG $\HH_1$
such that $L(\HH_1) = L(\G) \setminus \{\varepsilon\}$ and $\HH_1$ does
not contain a production of the form $A \rightarrow \varepsilon$. By
inspection of the construction we obtain that also $\HH_1$ is unambiguous.

Now let ${\cal A}$ be a deterministic finite-state string automaton
such that $L({\cal A}) = R$. Then we can apply the construction of
\cite[Thm.8.1]{barpersha61} to $\HH_1$ and ${\cal A}$ and obtain an unambiguous CFG $\HH_2$ with $L(\HH_2) = L(\HH_1) \cap R$. Let $Z$ be the initial nonterminal of $\HH_2$. Finally, from $\HH_2$ we can construct the unambiguous CFG $\G'$ as follows:
if $\varepsilon \in L(\G) \cap R$, then we add the new  initial
nonterminal $Z'$ and the  productions $Z' \rightarrow Z$ and  $Z'
\rightarrow \varepsilon$ to $\HH_2$, otherwise let $\G' = \HH_2$. It
is clear that $\G'$ is unambiguous and $L(\G') = L(\G) \cap R$.
\end{proof}

As consequence of  Lemmas  \ref{th:mezwri} and \ref{lm:closure} and of the result of  Chomsky-Sch\"utzenberger for context-free languages  we can now derive the result of  Chomsky-Sch\"utzenberger for quantitative context-free languages.%

{\em Proof of Theorem \ref{th:char}:} $1 \Leftrightarrow 3$: Immediate by Lemmas \ref{th:mezwri} and \ref{lm:closure}.

$2 \Rightarrow 3$: by Observation \ref{ob:Dyck}.

$3 \Rightarrow 2$: By the classical result of Chomsky-Sch\"utzenberger (cf. e.g. \cite[Thm.G1]{koz97})
there are an alphabet $Y$, a recognizable  language $R$ over $Y \cup
\overline{Y}$, and an alphabetic morphism $g: Y \cup \overline{Y}
\rightarrow \Delta \cup \{\varepsilon\}$  such that $L(\G) = g(D_Y
\cap R)$. By analysis of the construction, we have that the set $g^{-1}(v) \cap D_Y \cap R$ is in a one-to-one correspondence with $D_\G(v)$, for every $v \in L(\G)$. Since $\G$ is unambiguous, we have that $|g^{-1}(v) \cap D_Y \cap R| = 1$.

Next we prove that $(h\circ g(v') \mid v' \in \D_Y \cap R)$ is locally
finite in case $K$ is not complete. Since $h(L(\G))$ is defined, the set $I_w = \{v \in L(\G)
\mid (h(v),w) \not= 0\}$ is finite for every $w \in \Sigma^*$. Since
$g^{-1}(v)\cap D_Y \cap R$ is a singleton for every $v \in L(\G)$, the set $\{v' \in \D_Y \cap R \mid (h(g(v')),w)  \not= 0\}$
is finite for every $w \in \Sigma^*$. Hence $(h\circ g(v') \mid v' \in
\D_Y \cap R)$ is locally finite.

Thus $h \circ g: Y \cup \overline{Y} \rightarrow  K\langle\Sigma \cup \{\varepsilon\}\rangle$ is an alphabetic morphism,  $(h \circ g)(D_Y \cap R)$ is well defined, and $s = (h \circ g)(D_Y \cap R)$.

$3 \Rightarrow 4$: trivial.

$4 \Rightarrow 1$: by Lemma \ref{lm:closure}.
\hfill $\Box$

%
\section{Context-Free Step Functions}

An important result in the theory of rational formal power series states
that recognizable series over a semiring in which both operations  are
restricted to be locally finite, are recognizable step
functions \cite[Thm.11]{drostuvog10}. Here we investigate this concept
for context-free step functions over unital valuation monoids $K$.

If $L\subseteq\Sigma^*$ and $a\in K$, we let $a\cdot\one_L\in K\fl\Sigma^*\fr$ be the series satisfying $(a\cdot\one_L,w)=a$ if $w\in L$, and $(a\cdot\one_L,w)=0$ otherwise.

Let $s\in K\fl\Sigma^*\fr$. We say that $s$ is a \emph{context-free step function} if
$s = \sum_{i=1}^n a_i \cdot \one_{L_i}$ for some $n \in \nat$,
$a_1,\ldots,a_n \in K$, and context-free languages $L_1,\ldots,L_n
\subseteq \Sigma^*$. The languages $L_i$ are called {\em step
  languages}. Moreover, a context-free step function is a {\em
  recognizable step function} if each $L_i$ is recognizable.





As is well known, a recognizable step function over any semiring is a
recognizable series \cite[Ch.VI, Sec.7]{eil74}. This even holds for strong bimonoids with the same proof \cite[Lemma 8]{drostuvog10}, and could be extended to unital valuation monoids. In contrast, this implication fails for context-free languages and quantitative context-free languages.

\begin{ob}\label{ex:inh-amb} Let $L$ be an inherently ambiguous context-free
  language. Then $\one_L \not\in \CF(\Sigma,\mathbb{N})$.
\end{ob}
\begin{proof} Assume that $\one_L \in \CF(\Sigma,\mathbb{N})$. Then let $\G$ be a WCFG such that   $\one_L = \beh \G \beh$. Then, for every word $w \in L$, we have   that $|D_\G(w)| =1$, because otherwise the weights of different
  derivations of $w$ would sum up to a value greater than 1. But then
  the CFG which is underlying $\G$ is an unambiguous CFG for $L$,
  which contradicts to our assumption on $L$.
\end{proof}

However under suitable restrictions we obtain the  following positive result.

\begin{lm}\label{lm:1=cfstep} Let $L$ be a context-free language over
  $\Sigma$  and $a \in K$. If $L$   can be generated by some
  unambiguous CFG or if $K$ is complete and completely idempotent, then $a \cdot \one_L \in \CF(\Sigma,K)$.
\end{lm}

\begin{proof} We choose a new symbol $\# \not\in \Sigma$ and define
  the context-free  language $L' = \{\#w \mid w \in L\}$ over $\Sigma'
  = \Sigma \cup \{\#\}$. Moreover, we define the alphabetic morphism
  $h: \Sigma' \rightarrow K\langle \Sigma \cup \{\varepsilon\}\rangle$
  by $h(\#) = a.\varepsilon$ and $h(\sigma) = 1.\sigma$ for every
  $\sigma \in \Sigma$.

Clearly, if $L$ can be generated by some unambiguous CFG, then this
also holds for $L'$. Moreover, $(h(v) \mid v\in L')$ is locally finite
in case $K$ is not complete.  It follows that $a\cdot \one_L = h(L')$.  By Lemma
\ref{lm:closure} we obtain that $h(L') \in \CF(\Sigma,K)$.
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\end{proof}

We call a context-free step function a {\em context-free step function
  with unambiguous step languages} if each of its step languages can be
generated by an unambiguous CFG.


\begin{cor}\label{cor:CF-QCF} Let $s \in K\fl \Sigma^*\fr$ be a context-free step
  function. Let $s$ have unambiguous step languages or let $K$ be
  complete and completely idempotent. Then $s \in \CF(\Sigma,K)$.
\end{cor}
\begin{proof} The statement follows from Lemmas \ref{lm:1=cfstep} and  \ref{lm:WPDA-sum} and Theorem \ref{th:PDA=CF}.
\end{proof}

A context-free step function $s = \sum_{i=1}^n a_i \cdot \one_{L_i}$
is called \emph{strong} if the family $(L_i  \mid 1 \le i \le n)$
forms a partition of $\Sigma^*$, i.e.,  $L_i \cap L_j = \emptyset$ for
every $i \not= j$, and $\Sigma^* = \bigcup_{i=1}^n L_i$.


\begin{ob} Let $s \in K\fl\Sigma^*\fr$ be a power series. The following statements are equivalent:
\begin{enumerate}
\item $s$ is a strong context-free step function.
\item $\im(s)$ is finite and $s^{-1}(a)$ is a context-free language for every $a \in \im(s)$.
\end{enumerate}
\end{ob}

Due to the closure properties of the class of recognizable languages,
we can transform every recognizable step function over $\Sigma^*$ into an equivalent
one for which the collection of its step languages partitions
$\Sigma^*$. This is different for context-free step functions.

\begin{ob}\rm There are context-free series which are context-free step
functions  but  not strong context-free step functions.
\end{ob}
\begin{proof} For this
consider, e.g., the context-free step function $s = 1\cdot \one_{L_1}
+ 2 \cdot \one_{L_2}$ over the semiring of natural numbers with $L_1 =
\{a^nb^nc^k \mid n,k \in \nat\}$ and $L_2 = \{a^kb^nc^n \mid n,k \in
\nat\}$. (Recall from Example \ref{ex:val} that we can view any
semiring as a particular unital valuation monoid.). Since $L_1$ and
$L_2$ can be generated by unambiguous CFG, we obtain from Corollary
\ref{cor:CF-QCF} that $s$ is a context-free series. But $3 \in \im(s)$ and  $s^{-1}(3) = \{a^nb^nc^n \mid n \in \nat\}$ which is not context-free. \end{proof}




In the rest of this section we will prove a converse of Corollary \ref{cor:CF-QCF}.
%
%
We say that $K$ is \emph{locally finite}, if whenever $F\subseteq K$ is a finite subset, then the set $\Val(F^*)$ comprising the valuations of all finite sequences of elements of $F$ is finite.

\begin{ex}\rm
1. Consider a calculator and let $K$ be its (finite) set of nonnegative storable numbers. Then $(K,\sup,\mathrm{avg},0)$ is a finite valuation monoid. If we apply the procedure of Example \ref{ex:val}(1), we obtain a finite completely idempotent unital valuation monoid which is not a unital monoid-magma.

2. Consider the unital valuation monoid $K=(\mathbb{R} \cup \{-\infty,\infty\}, \sup, \mathrm{avg}', -\infty,\infty)$ where $\mathrm{avg}'$ is $\mathrm{avg}$ followed by truncation to a number having a prescribed bounded decimal expansion. Then $K$ is infinite, completely indempotent, and locally finite. This describes a situation where we may have exact input data and exact $\mathrm{avg}$ computation, but an output only of sufficient bounded precision.

3. A strong bimonoid $(K,+,\cdot,0,1)$ is called \emph{multiplicatively locally finite}, if whenever $F\subseteq K$ is a finite subset, then the submonoid $\gen{F}$ of $(K,\cdot,1)$ generated by $F$ is finite, cf. \cite{drovog12} for examples. Then a strong bimonoid $K$ is multiplicatively locally finite if and only if its associated valuation monoid (cf. Example \ref{ex:val}(4)) is locally finite.
\end{ex}

Now we show:

\begin{theo}\label{lm:WPDA-cfstep} Let $K$ be an additively
  idempotent, locally finite unital valuation monoid. Assume
  that $K$ is completely idempotent in case that $K$ is complete. Then
  each series $s \in \CF(\Sigma,K)$ is a context-free step function.
\end{theo}
\begin{proof} Due to Theorem \ref{th:PDA=CF}, there is a WPDA $\M = (Q,\Gamma,q_0,\gamma_0,F,T,\wt)$ over $\Sigma$ and $K$ such that $\beh \M \beh = s$. Clearly, $\wt(T)$ is a finite subset of $K$. Let $Y=\Val(\wt(T)^*)$. Then $Y$ is  finite. Also note that $\wt(\theta) \in Y$ for every computation $\theta$ of $\M$.

Let $w \in \Sigma^*$. Then
\[
(\beh \M\beh,w) = \sum_{\theta \in \Theta(w)} \wt(\theta) = \sum_{a \in Y}  \sum_{\substack{\theta \in \Theta(w)\\\wt(\theta) = a}} \wt(\theta) =^{*} \sum_{a \in Y} a \cdot \one_{L_a}(w)
\]
where $L_a = \{v \in \Sigma^* \mid \text{there is a $\theta \in
  \Theta(v)$ with $\wt(\theta)=a$}\}$. The equation marked by $*$
holds because $K$ is  additively idempotent, respectively, completely
idempotent in case $K$ is complete. It remains to prove that $L_a$ is context-free for every $a \in Y$.

We construct the PDA $\M_a = (Q',\Gamma,q_0',\gamma_0,F',T')$ where $Q' = Q \times Y$, $q_0' = (q_0,1)$, and $F' = F \times \{a\}$. Moreover, we let
\begin{align*}
T' =\  \{&((q,y),x,\gamma,(p,y'),\pi)  \mid  \tau = (q,x,\gamma,p,\pi) \in T,\text{ there are }\\
& w,v\in\Sigma^*,\mu\in\Gamma^*,\text{and a computation }\theta\text{ of }\M\text{ such that }\\
& (q_0,w,\gamma_0)\stackrel{\theta}{\vdash}(q,xv,\gamma\mu),y=\wt(\theta),\text{ and }y'=\wt(\theta\tau)\}\enspace.
\end{align*}
 Then $q_0'$-computations of $\M_a$ correspond to $q_0$-computations $\theta$ of $\M$ with $\wt(\theta)=a$, and conversely. It follows that $L(\M_a)= L_a$, hence $L_a$ is a context-free language.
\end{proof}

Note that  in the previous theorem, in general $s$ is not a strong context-free step function, because $L_a$ and $L_{a'}$ need not be disjoint.

A lattice is called {\em complete} if any subset has a supremum and
infimum. Trivially, every complete bounded lattice is a completely
idempotent and multiplicatively locally finite strong bimonoid, hence a locally finite unital valuation monoid. So,
as a consequence of Corollary \ref{cor:CF-QCF} and Theorem
\ref{lm:WPDA-cfstep}, we obtain immediately the following.

\begin{cor}\label{cor:bounded-lattices} Let $K$ be a complete bounded lattice and $s \in  K\fl\Sigma^*\fr$. Then $s \in \CF(\Sigma,K)$ if and only if $s$ is a context-free step function.
\end{cor}



%
\section{Conclusion and Open problems}

We could show that a fundamental result of formal language theory, the Chomsky-Sch\"utzenberger theorem, holds not only in semiring-weighted settings, but even for much more general computation models, the unital valuation monoids, which include, e.g., computations of averages of real numbers.
We can represent the quantitative languages by weighted context-free grammars and by weighted pushdown automata; both formalisms were shown to be expressively equivalent.
Finally, we considered context-free step functions.

In \cite[Thm.11]{drostuvog10} it was proved that every recognizable series over any additively locally finite and multiplicatively locally finite strong bimonoid is a recognizable step function. In the light of this result, we wonder whether it is possible to extend our Theorem \ref{lm:WPDA-cfstep} to additively locally finite strong bimonoids (while keeping the restriction on the multiplication operation).



\bibliographystyle{plain}
%
%
%

\input{CST4.bbl}

\end{document}

CST4.bbl
\begin{thebibliography}{10}

\bibitem{autberboa97}
J.~Autebert, J.~Berstel, and L.~Boasson.
\newblock Context-free languages and pushdown automata.
\newblock In G.~Rozenberg and A.~Salomaa, editors, {\em Handbook of Formal
  Languages, Vol. 1: Word, Language, Grammar}, volume~1, pages 111--174.
  Springer-Verlag, 1997.

\bibitem{barpersha61}
Y.~{Bar--Hillel}, M.~Perles, and E.~Shamir.
\newblock On formal properties of simple phrase structure grammars.
\newblock {\em Z. Phonetik. Sprach. Komm.}, 14:143--172, 1961.

\bibitem{berreu88}
J.~Berstel and C.~Reutenauer.
\newblock {\em Rational Series and Their Languages},
\newblock volume 12 of {\em EATCS Monographs on Theoretical Computer Science}. \newblock Springer-Verlag, 1988.

\bibitem{bir67}
G.~Birkhoff.
\newblock {\em Lattice Theory}.
\newblock AMS, 1967.

\bibitem{chadoyhen09a}
K.~Chatterjee, L.~Doyen, and Th. Henzinger.
\newblock Composition and alternation for weighted automata.

\bibitem{chadoyhen08}
K.~Chatterjee, L.~Doyen, and Th. Henzinger.
\newblock Quantitative languages.
\newblock {\em ACM Transactions on Computational Logic},
Vol. 11, No. 4, Article 23, 2010.
%\newblock In M.~Kaminski and S.~Martini, editors, {\em Proc. of the 17th
%  International Conference on Computer Science Logic (CSL 2008)}, volume 5213
%  of {\em Lecture Notes in Comput. Sci.}, pages 385--400. Springer-Verlag,
%  2008.

\bibitem{chadoyhen09}
K.~Chatterjee, L.~Doyen, and Th. Henzinger.
\newblock Expressiveness and closure properties for quantitative languages.
\newblock In {\em Proc. of 24th Annual IEEE Symposium on Logic in Computer
  Science (LICS 2009)}, pages 199--208. IEEE Computer Society, 2009.

\bibitem{chadoyhen09b}
K.~Chatterjee, L.~Doyen, and Th. Henzinger.
\newblock Probabilistic weighted automata.
\newblock In M.~Bravetti and G.~Zavattaro, editors, {\em Proc. of the 20th
  International Conference on Concurrency Theory (CONCUR 2009)}, volume 5710 of
  {\em Lecture Notes in Comput. Sci.}, pages 244--258. Springer-Verlag, 2009.

\bibitem{chavel12}
K.~Chatterjee and Y.~Velner.
\newblock Mean-payoff pushdown games.
\newblock Technical report, Institute of Science and Technology Austria, 2012.
\newblock Technical Report No. IST-2012-0002.

\bibitem{chosch63}
N.~Chomsky and M.P. Sch{\"u}tzenberger.
\newblock The algebraic theory of context-free languages.
\newblock In P.~Braffort and D.~Hirschberg, editors, {\em Computer Programming
  and Formal Systems}, pages 118--161. North-Holland, Amsterdam, 1963.

\bibitem{drogas07}
M.~Droste and P.~Gastin.
\newblock Weighted automata and weighted logics.
\newblock {\em Theor. Comput. Sci.}, 380(1-2):69--86, 2007.

\bibitem{dromei10}
M.~Droste and I.~Meinecke.
\newblock Describing average- and longtime-behavior by weighted {MSO} logics.
\newblock In {\em Mathematical Foundations of Computer Science (MFCS)}, volume 6281 of {\em Lecture Notes in Computer Science},  pages 537--548. Springer, 2010.

\bibitem{dromei11}
M.~Droste and I.~Meinecke.
\newblock Weighted automata and regular expressions over valuation monoid.
\newblock {\em Intern. J. of Foundations of Comp. Science}, 22 (2011), 1829-1844. Selected papers of CIAA 2010.

\bibitem{drostuvog10}
M.~Droste, T.~St\"uber, and H.~Vogler.
\newblock Weighted finite automata over strong bimonoids.
\newblock {\em Information Sciences}, 180:156--166, 2010.

\bibitem{drovog12}
M.~Droste and H.~Vogler.
\newblock Weighted automata and multi-valued logics over arbitrary bounded
  lattices.
\newblock {\em Theoretical Computer Science}, 418, 2012, 14-36.

\bibitem{eil74}
S.~Eilenberg.
\newblock {\em Automata, Languages, and Machines -- Volume A}, volume~59 of
  {\em Pure and Applied Mathematics}.
\newblock Academic Press, 1974.

\bibitem{gol99}
J.S. Golan.
\newblock {\em Semirings and their Applications}.
\newblock Kluwer Academic Publishers, Dordrecht, 1999.

\bibitem{gra03}
G.~Gr\"atzer.
\newblock {\em General Lattice Theory}.
\newblock Birkh\"auser Verlag, Basel, 2003.

\bibitem{koz97}
D.~Kozen.
\newblock {\em Automata and Computability}.
\newblock Springer-Verlag, 1997.

\bibitem{kuisal86}
W.~Kuich and A.~Salomaa.
\newblock {\em Semirings, Automata, Languages}, volume~5 of {\em Monogr.
  Theoret. Comput. Sci. EATCS Ser.}
\newblock Springer-Verlag, 1986.


\bibitem{mei11}
I. Meinecke. 
\newblock Valuations of weighted automata: Doing it in a rational way.
\newblock In: W. Kuich, G. Rahonis, editors, {\em Algebraic Foundations in Computer Science},  volume 7020 of {\em Lecture Notes in Computer Sciences}, Springer, 2011, pp. 309-346. 


\bibitem{petsal09}
I.~Petre and A.~Salomaa.
\newblock Algebraic systems and pushdown automata.
\newblock In M.~Droste, W.~Kuich, and H.~Vogler, editors, {\em Handbook of
  {W}eighted {A}utomata}, chapter~7, pages 257--311. Springer-Verlag, 2009.

\bibitem{salsoi78}
A.~Salomaa and M.~Soittola.
\newblock {\em Automata-Theoretic Aspects of Formal Power Series}.
\newblock Texts and Monographs in Computer Science, Springer-Verlag, 1978.

\bibitem{sch61}
M.P.~Sch\"utzenberger.
\newblock {\em On the definition of a family of automata}.
\newblock Inf. and Control 4, 245--270 (1961).

\end{thebibliography}

