package universo

  1. Overview
  2. Docs
include Kernel.Reduction.ConvChecker

are_convertible sg t1 t2 checks whether t1 and t2 are convertible or not in the signature sg.

constraint_convertibility cstr r sg [t1] [t2] checks wehther the [cstr] of the rule [r] is satisfiable. Because constraints are checked once a term has matched the pattern, satisfying a constraint comes back to check that two terms are convertible

conversion_step sg (l,r) lst returns a list lst' containing new convertibility obligations. Raise NotConvertible if the two terms are not convertible.

reduction cfg sg te reduces the term te following the configuration cfg and using the signature sg.

whnf sg t returns the Weak Head Normal Form of t.

Definition: a term is in weak-head-normal form if there is a reduction strategy such that all its reducts following this strategy (including itself) have the same 'shape' at the root.

The shape of a term could be computed like this:

let rec shape = function | Type -> Type | Kind -> Kind | Pi _ -> Pi | Lam _ -> Lam | DB (_,_,n) -> DB n | Const (_,m,v) -> Const m v | App(f,a0,args) -> App (shape f,List.length (a0::args))

Property: A (strongly normalizing) non weak-head-normal term can only have the form:

  • (x:A => b) a c_1..c_n, this is a beta-redex potentially with extra arguments.
  • or c a_1 .. a_n b_1 ..b_n with c a constant and c a'_1 .. a'_n is a gamma-redex where the (a'_i)s are reducts of (a_i)s.

sng sg t returns the Strong Normal Form of t. This may loop whenever t is not strongly normalizing.

OCaml

Innovation. Community. Security.