Displaying similar documents to “Extending the lambda-calculus with unbind and rebind”

Extending the lambda-calculus with unbind and rebind

Mariangiola Dezani-Ciancaglini, Paola Giannini, Elena Zucca (2011)

RAIRO - Theoretical Informatics and Applications

Similarity:

We extend the simply typed -calculus with and primitive constructs. That is, a value can be a fragment of open code, which in order to be used should be explicitly rebound. This mechanism nicely coexists with standard static binding. The motivation is to provide an unifying foundation for mechanisms of , where the meaning of a name is determined at runtime, , such as dynamic updating of resources and exchange of mobile code, and , where an alternative action is taken if a binding...

Extension of Reverse Elimination Method Through a Dynamic Management of the Tabu List

Saïd Hanafi, Arnaud Fréville (2010)

RAIRO - Operations Research

Similarity:

The Reverse Elimination Method (REM) is a dynamic strategy for managing the tabu list. It is based on logical interdependencies between the solutions encountered during recent iterations of the search. REM provides both a necessary and sufficient condition to prevent cycling. The purpose of this paper is first to incorporate in REM a when cycling is unavoidable, thereby assuring the finite convergence of Tabu Search. Secondly, we correct a generalization of REM, the so-called REM-...

Pointwise constrained radially increasing minimizers in the quasi-scalar calculus of variations

Luís Balsa Bicho, António Ornelas (2014)

ESAIM: Control, Optimisation and Calculus of Variations

Similarity:

We prove of vector minimizers () =  (||) to multiple integrals ∫ ((), |()|)  on a  ⊂ ℝ, among the Sobolev functions (·) in + (, ℝ), using a  : ℝ×ℝ → [0,∞] with (·) and . Besides such basic hypotheses, (·,·) is assumed to satisfy also...

Easy lambda-terms are not always simple

Alberto Carraro, Antonino Salibra (2012)

RAIRO - Theoretical Informatics and Applications

Similarity:

A closed -term is if, for any other closed term , the lambda theory generated by  =  is consistent. Recently, it has been introduced a general technique to prove the easiness of -terms through the semantical notion of simple easiness. Simple easiness implies easiness and allows to prove consistency results construction of suitable filter models of -calculus living in the category of complete partial orderings: given ...

Trivial Cases for the Kantorovitch Problem

Serge Dubuc, Issa Kagabo, Patrice Marcotte (2010)

RAIRO - Operations Research

Similarity:

Let and be two compact spaces endowed with respective measures and satisfying the condition . Let be a continuous function on the product space . The mass transfer problem consists in determining a measure on whose marginals coincide with and , and such that the total cost be minimized. We first show that if the cost function is decomposable, i.e., can be represented as the sum of two continuous functions defined on and , respectively, then every feasible measure is optimal....

Easy lambda-terms are not always simple

Alberto Carraro, Antonino Salibra (2012)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

Similarity:

A closed -term is if, for any other closed term , the lambda theory generated by  =  is consistent. Recently, it has been introduced a general technique to prove the easiness of -terms through the semantical notion of simple easiness. Simple easiness implies easiness and allows to prove consistency results construction of suitable filter models of -calculus living in the category of complete partial orderings: given a simple easy term and an arbitrary closed term , it is possible to...

Hereditary properties of words

József Balogh, Béla Bollobás (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

Let be a hereditary property of words, , an infinite class of finite words such that every subword (block) of a word belonging to is also in . Extending the classical Morse-Hedlund theorem, we show that either contains at least words of length for every  or, for some , it contains at most words of length for every . More importantly, we prove the following quantitative extension of this result: if has words of length then, for every , it contains at most ⌈( + 1)/2⌉⌈( + 1)/2⌈...

Encoding FIX in Object Calculi

Roy L. Crole (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We show that the type theory introduced by Crole and Pitts [3] can be encoded in variants of Abadi and Cardelli's object calculi. More precisely, we show that the type theory presented with judgements of both equality and operational reduction can be translated into object calculi, and the translation proved sound. The translations we give can be seen as using object calculi as a metalanguge within which can be represented; an analogy can be drawn with Martin Löf's Theory of Arities...

Denotational aspects of untyped normalization by evaluation

Andrzej Filinski, Henning Korsholm Rohde (2010)

RAIRO - Theoretical Informatics and Applications

Similarity:

We show that the standard normalization-by-evaluation construction for the simply-typed -calculus has a natural counterpart for the untyped -calculus, with the central type-indexed logical relation replaced by a “recursively defined” , in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal forms,...