ocamllambda-calculus

how to implement lambda-calculus in OCaml?


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.


Solution

  • 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#?.