then there exist ? and U such that ,
By the fact that ? ? ? is defined point-wise ,
Therefore, there exists ? ? ? such that ? M : A. By Theorem 2, M is strongly normalising. 3. ? Assume F ? x ? . Then, there exists ? ? ? such that ? x, We also have ?(x) ? ?(x). Hence, F ? ?(x) ,
Then, (x : F ) ? ? and x : F x : F . Therefore, F ? x ? ,
Therefore, there exist ? 1 , ? 2 and A such that ? = ? 1 ? ? 2 , ? 1 M : A ? F and ? 2 N : A ,
Computational interpretations of linear logic, Theoret. Comput. Sci, vol.111, pp.3-57, 1993. ,
A term calculus for intuitionistic linear logic, Proc. of the 1st Int. Conf. on Typed Lambda Calculus and Applications, pp.75-90, 1993. ,
A filter lambda model and the completeness of type assignment, Ber09] A. Bernadet. Fixpoints and strong normalisation. Internship report, pp.931-940, 1983. ,
DOI : 10.1002/malq.19800261902
Complexity of strongly normalising ?-terms via non-idempotent intersection types, Proc. of the 14th Int. Conf. on Foundations of Software Science and Computation Structures (FOSSACS'11), pp.46-47, 2011. ,
Filter models: non-idempotent intersection types, orthogonality and polymorphism Non-idempotent intersection types and strong normalisation Soft lambda-calculus: a language for polynomial time computation. CoRR, cs Alcune proprietà delle forme ?-?-normali nel ?K-calcolo, Proc. of the 20th Annual Conf. of the European Association for Computer Science Logic (CSL'11), LIPIcs. Schloss Dagstuhl LCI Dezani-Ciancaglini. A new type assignment for lambda-terms. Archiv für mathematische Logik und Grundlagenforschung, pp.61-68, 1968. ,
Intuitionism: an introduction. Studies in logic and the foundations of mathematics, 1971. ,
The formulae-as-types notion of construction, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp.479-490, 1980. ,
A prismoid framework for languages with resources, Theoretical Computer Science, vol.412, issue.37, pp.4867-4892, 2011. ,
DOI : 10.1016/j.tcs.2011.01.026
URL : https://hal.archives-ouvertes.fr/hal-00625598
Combinatory reduction systems: introduction and survey Principality and decidable type inference for finite-rank intersection types, Proc. of the 26th Annual ACM Symp. on Principles of Programming Languages (POPL'99) Lafont. Soft linear logic and polynomial timeLei86] D. Leivant. Typing and computational properties of lambda expressions Lawvere and S. H. Schanuel. Conceptual Mathematics: A First Introduction to Categories, pp.279-308, 1986. ,
Types, potency, and idempotency: why nonlinearity and amnesia make a type system work Nominal logic, a first order theory of names and binding, Proc. of the 9th ACM Intern. Conf. on Functional Programming, pp.138-149, 2003. ,
Les ressources explicites vues par la théorie de la réécriture, p.36, 2011. ,
On the Membership Problem for Non-Linear Abstract Categorial Grammars Domains for denotational semantics, J. of Logic, Language, and Information Lecture Notes in Computer Science, vol.19, issue.140 8, pp.163-183, 1982. ,
Domains for denotational semantics, Proc. of the 9th Intern, pp.577-613, 1982. ,
A realizability interpretation of the theory of species On computable numbers, with an application to the Entscheidungsproblem Intersection Type Assignment Systems, Logic ColloquiumvH02] J. van Heijenoort. From Frege to Gödel : A Source Book in Mathematical LogicSource Books in the History of the Sciences), pp.240-251, 1936. ,
Perpetual Reductions in??-Calculus, Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS), pp.173-225, 1996. ,
DOI : 10.1006/inco.1998.2750
Var ? Term, we define bind(M, f ) the term defined by induction on M as follow: bind(x, f ) = f (x) bind(M N, f ) = bind(M, f )bind(N, f ) bind(?M, f ) = ?bind(M, f ) with f : Var ? Term the unique function such that, (x)) (?x ? Var ,
Then f : Var ? Term and bind(M, f ) = map(M, f ) ,
Then for all f, g : Var ? Term, if we have ?x ? fv(M ), f (x) = g(x) then bind(M, f ) = bind(M, g) ,
Assume M ? Term and f : Var ? Var, Then fv(map(M, f )) = {f (x) | x ? fv(M )} ,
Then: fv(bind(M, f )) = x?fv(M ) fv(f (x)) ,
Assume M ? Term, f : Var ? Var and g : Var ? Term. Then g ? f : Var ? Term and bind(map(M, f ), g) = bind(M, g ? f ) ,
f : Var ? Term, and g : Var ? Term We write h : Var ? Term defined by: ?x ? Var, h(x) = bind(f (x), g) Then we have bind(bind, g) = bind(M, h) ,
We write M {x := N } for bind(M, f ) with f : Var ? Term defined as follow: f (x) = N f (y) = ,
? Term and x, y ? Var, Then: ? If x / ? fv(M ), then M {x := N } = M ,
We write ?x ,
N then M {x := y} = N and if x = y then y / ? fv(M ) ,
For all x, y ? Var we define < x, y >: Var ? Var defined as follow ,
Then M = N if and only if M = ? N ,
One way is by induction on M ? T Var and the other way is by induction on M = ? N ,
f : Var ? Term, and M ? Term such that for all x ? fv(M ), [f (x)] ?1 = ? 2 (x) ? ?, Then [bind(M, f )] ?1 = [M ] ?2 ? ? ,
Then [M {x := N }] ? = [M ] ? with ? ? Env X defined as follow: ? (x) = ,