package lambda

  1. Overview
  2. Docs

Module Lambda.LSource

Sourcetype term =
  1. | Var of string
  2. | Abs of string * term
  3. | App of term * term
    (*

    lambda term type definition

    *)
Sourceval get_var : int -> string

get_var i returns a var identified by its index i

Sourcetype 'a set =
  1. | Set of 'a list
    (*

    set used for free variables

    *)
Sourceval fv : term -> string set

fv t returns free variables of t

Sourceval fv_l : term -> string list

fv_l t returns free variables of t as a list

Sourceval to_string : term -> string

to_string t converts a term to its string representation

Sourceval eta_conversion : term -> term

eta_conversion t applies η-conversion to t, if applicable

Sourceval alfa_conversion : string -> string -> term -> term

conversion a b t applies α-conversion to t replacing variable a with variable b

Sourceval reduce_fix : term -> term

reduce_fix t applies β-reduction until there is no other reduction applicable

Sourceval reduce_fix_timeout : ?n:int -> term -> term

reduce_fix_timeout n t applies β-reduction until there is no other reduction * applicable or until n iterations reached

Sourceval reduce : int -> term -> term

reduce n t applies n steps of β-reduction to t

Sourceval has_redex : term -> bool

has_redex t returns true if t has a β-reduction step

Sourceval subst : string -> term -> term -> term

subst v t' t

Sourceval len : term -> int

len t returns the length of t

OCaml

Innovation. Community. Security.