In OCaml, it seems that "fun" is the binding operator to me. Does OCaml have built-in substitution? If does, how it is implemented? is it implemented using de Bruijn index?
Just want to know how the untyped lambda-calculus can be implemented in OCaml but did not find such implementation.
OCaml does not perform normal-order reduction and uses call-by-value semantics. Some terms of lambda calculus have a normal form than cannot be reached with this evaluation strategy.
See The Substitution Model of Evaluation, as well as How would you implement a beta-reduction function in F#?.