“Rewriting rules” refers to term-rewriting systems[1], which are sets of directed equations. An “undirected” equation is similar to what you see grade-school algebra class, e.g. y = ax + b; if you have the right pieces of data, you can solve the equation towards either side of the equals sign. A directed equation can only be solved in one direction. That’s important because it allows you to come up with a system of rules that, when recursively applied to a term, eventually terminate.
A “confluent” term rewriting system just means that the set of equations in that TRS has a property where, if there’s ever multiple applicable rules that can be applied, no matter which of those rules you choose to apply to a term, you eventually get to the same state (again, when the rules are applied repeatedly to a term).
Beta-reduction [2] is one of the core operations you can perform with lambda calculus? You can think of it as being equivalent to a function call; an alternate analogy is when a C compiler inlines a particular function call during compilation, it’s performing beta-reduction at that call site.
That doesn’t explain everything in the quoted text, but hopefully it helps make it a bit more understandable. If you really want to learn more about this area of CS, take a look at the book Types and Programming Languages (TAPL) [3].
A “confluent” term rewriting system just means that the set of equations in that TRS has a property where, if there’s ever multiple applicable rules that can be applied, no matter which of those rules you choose to apply to a term, you eventually get to the same state (again, when the rules are applied repeatedly to a term).
Beta-reduction [2] is one of the core operations you can perform with lambda calculus? You can think of it as being equivalent to a function call; an alternate analogy is when a C compiler inlines a particular function call during compilation, it’s performing beta-reduction at that call site.
That doesn’t explain everything in the quoted text, but hopefully it helps make it a bit more understandable. If you really want to learn more about this area of CS, take a look at the book Types and Programming Languages (TAPL) [3].
[1] https://en.m.wikipedia.org/wiki/Rewriting
[2] https://en.m.wikipedia.org/wiki/Lambda_calculus#β-reduction
[3] https://www.cis.upenn.edu/~bcpierce/tapl/