The meaning of a judgment is explained in terms of the computation of the types and terms in the judgment. These computations stop when a canonical form is reached. By canonical form we mean a term where the outermost form is a constructor (introduction form). These are the canonical forms used in lazy functional programming (for example in the Haskell language).