Wyniki wyszukiwania - BazTech

1

Two Squares of Oppositions and Their Applications in Pairwise Comparisons Analysis

Schumann A., Woleński J.

Fundamenta Informaticae

|

2016

|

Vol. 144, nr 3/4

241--254

EN

This paper examines two main possibilities of pairwise comparisons analysis: first, pairwise comparisons within a lattice, in this case these comparisons can be measurable by numbers; second, comparisons beyond any lattice, in this case these comparisons cannot be measurable in principle. We show that the first approach to pairwise comparisons analysis is based on the conventional square of opposition and its generalization, but the second approach is based on unconventional squares of opposition. Furthermore, the first approach corresponds to lateral inhibition in transmission signals and the second approach corresponds to lateral activation in transmission signals.

2

The Impact of seq on Free Theorems-Based Program Transformations

Johann P., Voigtländer J.

Fundamenta Informaticae

|

2006

|

Vol. 69, nr 1,2

63-102

EN

Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, standard parametricity results - including so-called free theorems - fail for nonstrict languages supporting a polymorphic strict evaluation primitive such as Haskell's seq. A folk theorem maintains that such results hold for a subset of Haskell corresponding to a Girard-Reynolds calculus with fixpoints and algebraic datatypes even when seq is present provided the relations which appear in their derivations are required to be bottom-reflecting and admissible. In this paper we show that this folklore is incorrect, but that parametricity results can be recovered in the presence of seq by restricting attention to left-closed, total, and admissible relations instead. The key novelty of our approach is the asymmetry introduced by left-closedness, which leads to ``inequational'' versions of standard parametricity results together with preconditions guaranteeing their validity even when seq is present. We use these results to derive criteria ensuring that both equational and inequational versions of short cut fusion and related program transformations based on free theorems hold in the presence of seq.

3

Names, equations, relations : practical ways to reason about new

Stark I.

Fundamenta Informaticae

|

1998

|

Vol. 33, nr 4

369-396

EN

The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the from of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between names and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculus has connections to local declaations in general; to the mobile processes of the p-calculus; and to security protocols in the spi-calculus. This paper introduces a logic of equations and relations which allows one to reason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of contextual equivalence (also known as observational, or observable, equivalence). The logic based on earlier operational techniques, providing the same power but in a much more accessible from. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.