Local versus non-local functionals I'm new to field theory and I don't understand the difference between a "local" functional and a "non-local" functional. Explanations that I find resort to ambiguous definitions of locality and then resort to a list of examples. A common explanation is that local functionals depend on the value of the integrand "at a single point."
For instance, this functional is given as local, $$ F_1[f(x)] = \int_{a}^{b} dx f(x) $$ but this functional is not $$ F_2[f(x)] = \int_{a}^{b} \int_{a}^{b} dx dx' f(x) K(x, x') f(x') $$
To further compound my confusion, some references (see Fredrickson, Equilibrium Theory of Inhomogeneous Polymers) state that gradients make a functional non-local (or I have even heard the term semi-local), whereas others (see Why are higher order Lagrangians called 'non-local'?) state that gradients do not make a functional non-local.
Is there a more rigorous definition of locality?
 A: Yes, there are rigorous ways of defining locality in such contexts, but the precise terminology used unfortunately depends on both the context, and who is making the definition.
Let me give an example context and definition.
Example context/definition.
For conceptual simplicity, let $\mathcal F$ denote a set of smooth, rapidly decaying functions $f:\mathbb R\to \mathbb R$.  A functional $\Phi$ on $\mathcal F$ is a function $\Phi:\mathcal F\to \mathbb R$.
A function (not yet a functional on $\mathcal F$) $\phi:\mathcal F\to\mathcal F$ is called local provided there exists a positive integer $n$, and a function $\bar\phi:\mathbb R^{n+1}\to\mathbb R$ for which
\begin{align}
  \phi[f](x) = \bar\phi\big(x, f(x), f'(x), f''(x), \dots, f^{(n)}(x)\big) \tag{1}
\end{align}
for all $f\in \mathcal F$ and for all $x\in\mathbb R$.  In other words, such a function is local provided it depends only on $x$, the value of the function $f$ at $x$, and the value of any finite number of derivatives of $f$ at $x$.
A functional $\Phi$ is called an integral functional provided there exists a function $\phi:\mathcal F\to\mathcal F$ such that
\begin{align}
  \Phi[f] = \int_{\mathbb R} dx \, \phi[f](x). \tag{2}
\end{align}
An integral functional $\Phi$ is called local provided there exists some local function $\phi:\mathcal F\to\mathcal F$ for which $(2)$ holds.
What could we have defined differently?
Some authors might not allow for derivatives in the definition $(1)$, or might call something with derivatives semi-local.  This makes intuitive sense because if you think of Taylor expanding a function, say, in single-variable calculus, you get
\begin{align}
  f(x+a) = f(x) + f'(x)a + f''(x)\frac{a^2}{2} + \cdots,
\end{align}
and if you want $a$ to be large, namely if you want information about what the function is doing far from $x$ (non-local behavior), then you need more an more derivative terms to sense that.  The more derivatives you consider, the more you sense the "non-local" behavior of the function.
One can also generalize to situations in which the functions involved are on manifolds, or are not smooth but perhaps only differentiable a finite number of times etc., but these are just details and I don't think illuminate the concept.
Example 1 - a local functional.
Suppose that we define a function $\phi_0:\mathcal F\to \mathcal F$ as follows:
\begin{align}
  \phi_0[f](x) = f(x),
\end{align}
then $\phi_0$ is a local function $\mathcal F\to\mathcal F$, and it yields a local integral functional $\Phi_0$ given by
\begin{align}
  \Phi_0[f] = \int_{\mathbb R} dx\, \phi_0[f](x) = \int_{\mathbb R} dx\, f(x),
\end{align}
which simply integrates the function over the real line.
Example 2 - another local functional.
Consider the function $\phi_a:\mathcal F\to\mathcal F$ defined as follows:
\begin{align}
  \phi_a[f](x) = f(x+a).
\end{align}
Is this $\phi_a$ local?  Well, for $a=0$ it certainly is since it agrees with $\phi_0$.  What about for $a\neq 0$?  Well for such a case $\phi_a$ certainly is not because $f(x+a)$ depends both on $f(x)$ and on an infinite number of derivatives of $f$ at $x$.  What about the functional $\Phi_a$ obtained by integrating $\phi_a$?  Notice that
\begin{align}
  \Phi_a[f] 
  &= \int_{\mathbb R} dx\,\phi_a[f](x) \\
  &= \int_{\mathbb R} dx\, f(x+a) \\
  &= \int_{\mathbb R} dx\, f(x) \\
  &= \int_{\mathbb R} dx\, \phi_0[f](x)\\
  &= \Phi_0[f].
\end{align}
So $\Phi_a[f]$ is local even though $\phi_a$ is not for $a\neq 0$.  
The lesson of this example is this: you may encounter an integral functional $\Phi:\mathcal F\to\mathbb R$ that is defined by integrating over a non-local function $\phi:\mathcal F\to\mathcal F$.  However, there might still be a way of writing the functional $\Phi$ as the integral over a different function, say $\phi'$, that is local, in which case we can assert that $\Phi$ is local as well because to verify that a functional is local, you just need to find one way of writing it as the integral of a local function.
