Module Logtk.Lambda (.ml)

module Lambda: LogtkLambda

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 LogtkLambda.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.
Raises LogtkType.Error if types are not compatible
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