The Barrier of Objects: From Dynamical Systems to Bounded Organizations

作者: L.W. Buss , W. Fontana

DOI:

关键词: Type (model theory)Substitution (algebra)Order (ring theory)Dynamical systems theoryPhysicsDiscrete mathematicsExpression (computer science)Type theoryBounded functionVariable (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

参考文章(71)
Christian Retoré, Réseaux et séquents ordonnés Université Paris-Diderot - Paris VII. ,(1993)
J.-Y. Girard, Linear logic: its syntax and semantics Proceedings of the workshop on Advances in linear logic. pp. 1- 42 ,(1995) , 10.1017/CBO9780511629150.002
M. Sch�nfinkel, Über die Bausteine der mathematischen Logik Mathematische Annalen. ,vol. 92, pp. 305- 316 ,(1924) , 10.1007/BF01448013
Jean-Yves Girard, Paul Taylor, Yves Lafont, Proofs and types ,(1989)
V. Danos, L. Regnier, Proof-nets and the Hilbert space Proceedings of the workshop on Advances in linear logic. pp. 307- 328 ,(1995) , 10.1017/CBO9780511629150.016
Gerhard Gentzen, M. E. Szabo, The collected papers of Gerhard Gentzen ,(1969)
Robin Milner, Communication and Concurrency ,(1989)
Manfred Eigen, John McCaskill, Peter Schuster, The molecular quasi-species John Wiley & Sons, Inc.. pp. 149- 263 ,(2007) , 10.1002/9780470141243.CH4