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.
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.
