package logtk

  1. Overview
  2. Docs
On This Page
  1. Lambda-Calculus
Legend:
Library
Module
Module type
Parameter
Class
Class type

Lambda-Calculus

type term = LogtkHOTerm.t
type scope = LogtkSubsts.scope
val beta_reduce : ?depth:int -> term -> term

Beta-reduce the term

val eta_reduce : term -> term

Eta-reduce the term

val lambda_abstract : term -> sub:term -> term

lambda_abstract term ~sub, applied to a curried term term, and a subterm sub of term, gives term' such that beta_reduce (term' @ sub_t) == term holds. It basically abstracts out sub with a lambda. If sub is not a subterm of term, then term' == ^[X]: term.

For instance (@ are omitted), lambda_abstract f(a,g @ b,c) ~sub:g will return the term ^[X]: f(a, X @ b, c).

val lambda_abstract_list : term -> term list -> term

Abstract successively the given subterms, starting from the right ones. The converse operation is lambda_apply_list, that is, lambda_apply_list (lambda_abstract_list t args) args = t should hold.

val match_types : ?subst:LogtkSubsts.Ty.t -> LogtkType.t -> scope -> LogtkType.t list -> scope -> LogtkSubsts.t

Match the first type's arguments with the list.

val can_apply : LogtkType.t -> LogtkType.t list -> bool

Can we apply a term with the given type to terms with the corresponding list of types?

val lambda_apply_list : ?depth:int -> term -> term list -> term

Apply a lambda to a list of arguments. The type of the lambda must be a generalization of a function that takes the list's types as arguments.

  • raises LogtkType.Error

    if the first term doesn't have a function type or if the types are not compatible

OCaml

Innovation. Community. Security.