作者: L.W. Buss , W. Fontana
DOI:
关键词: Type (model theory) 、 Substitution (algebra) 、 Order (ring theory) 、 Dynamical systems theory 、 Physics 、 Discrete mathematics 、 Expression (computer science) 、 Type theory 、 Bounded function 、 Variable (mathematics)
摘要: ion Ax ∪ {x : τ ′} e A λx.e ′ → Let σ σ} e′ (let x = in e′) The meaning of the Taut-rule is simply that a free variable has type assigned to it boundary condition. If there no assignment expression not typable, and barred from universe. rule App also clear. It useful, however, know how implemented, since introduces an important concept. Suppose we have object whose been established be σ, want apply ′. For this possible must form where stands for generic unknown (e)e′ needs determined. Hence, interaction e’s required made equal. This may possible, contain variables which can more specific order satisfy equality. means look some substitution T such Tσ (τ τ). called unifier, procedure finding unification. boils down solving set equations. details about carried out reader referred any standard textbook on theory. point