longNormalForm
gapt.expr.util.longNormalForm
object longNormalForm
If t = λx₁...λxₘ(y u₁ ... uₚ) is a normal term of type T₁ → ... → Tₙ → U, with U atomic and m ≤ n, then its long normal form is the term
λx₁...λxₘλxₘ₊₁...λxₙ(y u₁'... uₚ' xₘ₊₁' ... xₙ'),
where uᵢ' is the long normal form of uᵢ and xⱼ' is the long normal form of xⱼ.
Implemented according to Definition 2.25, Higher-Order Unification and Matching by Gilles Dowek.
Attributes
- Source
- longNormalForm.scala
- Graph
-
- Supertypes
-
class Objecttrait Matchableclass Any
- Self type
-
longNormalForm.type
Members list
In this article