What is the definition of a redex and what are they for in programming languages literature?

Question

I saw the word "redex" in the context of proramming language theory/semantics in 2018 and now when I was reading a neurosymbolic research paper (machine learning with neural nets + symbolic algorithms).

The research paper said:

Constructing $I\beta'$ (operator that inverts one step of beta-reductions/function applications) depends on careful consideration of the reduction operator we aim to invert (see [39] and Appen- dix F). The operator $I\beta'$ builds both top-level redexes and also recurses to build redexes within the body of an expression

The 2018 course says:

In an RSEC language definition one starts by defining the syntax of evaluation contexts, or simply just contexts, which is typically done by means of a context-free grammar (CFG). A context is a program or a fragment of program with a hole, where the hole, which is written $\Box$ , is a placeholder for where the next computational step can take place. If $c$ is an evaluation context and $e$ is some well-formed appropriate fragment (expression, statement, etc.), then $c[e]$ is the program or fragment obtained by replacing the hole of $c$ by $e$. Reduction semantics with evaluation contexts relies on a tacitly assumed (but rather advanced) parsing mechanism that takes a program or a fragment $p$ and decomposes it into a context $c$ and a subprogram or fragment $e$, called a redex, such that $p = c[e]$. This decomposition process is called splitting (of $p$ into $c$ and $e$). The inverse process, composing a redex $e$ and a context $c$ into a program or fragment $p$, is called plugging (of $e$ into $c$). These splitting/plugging operations are depicted in Figure 3.28.

enter image description here

So is a redex just a fragment of a program? Is that all? Curious why this needs a term of its own. It's use and importance.

---

cross: https://www.quora.com/unanswered/What-is-the-definition-of-a-redex-and-what-are-they-for-in-programming-languages-theory

Answer 1

A redex is an expressions on which we can perform a computation step, such as:

1. fst (a, b) is a redex, it computes to a
2. snd (a, b) is a redex, it computes to b
3. (λ x . x + x) 6 is a redex, it computes to 6 + 6
4. if true then A else B is a redex, it computes to A

Here are some examples which are not redexes: fst p, if x < 6 then 3 else 4, 42, λ x . x + x.

An expression may contain a redex, for instance in

λ x . if x < 6 then fst (4, 5) else x

there is a redex, namely fst (4, 5). In general, an expression may contain main redexes. Which ones are evaluated and in what order depends on how the language is designed.