Wolfram Function as Lambda Calculus

Wolfram language, Function considered as a term rewriting rule

in Wolfram language, the paradigm it does computation is via term rewriting.

you create rewrite rules, then whenever during a evaluation of an expression such that parts matches the pattern, it get replaced by the rule.

For example, most user functions are defined this way

Clear[ ff ]

(* define a rule, replacing pattern ff[x_] to x + 1 *)
ff[x_] := x + 1

ff[3]
(* 4 *)

however, you can define a function in a pure function way, without defining a rewrite rule. For example:

(* a function to add 1 to arg, applied at 3 *)
Function[{x}, x + 1][3]
(* 4 *)

but how does one explain this function's method of computation in a term-rewriting system?

we might think of it this way:

by default, there is a builtin rule:

Function[x,body][y] := Replace[ body, x :> y ]

so that the function call pattern

Function[args][x]

always matches the rule during evaluation.

that's one way to explain how lambda works in Wolfram language via a pure term rewriting system.

but am not sure that is how it is actually implemented.

If we are trying to explain the whole Wolfram language as rewrite system, we also need to explain how 1 + 1 is computed. It can be theoretically explained by church numeral Church encoding. But is obviously not how it is done.

therefore, trying to explain Wolfram language's Function in terms of term rewriting may not be too useful.