Explicit Substitutions à la de Bruijn: the local and global way

Kamareddine and Nederpelt[9], resp. Kamareddine and Ríos [11] gave two calculi of explicit of substitutions highly influenced by de Bruijn's notation of the λ-calculus. These calculi added to the explosive pool of work on explicit substitution in the past 15 years. As far as we know, calculi of explicit substitutions: a) are unable to handle local substitutions, and b) have answered (positively or negatively) the question of the termination of the underlying calculus of substitutions. The exception to a) is the calculus of [9] where substitution is handled both locally and globally. However, the calculus of [9] does not satisfy properties like confluence and termination. The exception to b) is the λs_e-calculus of [11] for which termination of the s_e-calculus, the underlying calculus of substitutions, remains unsolved. This paper has two aims:

(i) To provide a calculus à la de Bruijn which deals with local substitution and whose underlying calculus of substitutions is terminating and confluent.

(ii) To pose the problem of the termination of the substitution calculus of [11] in the hope that it can generate interest as a termination problem which at least for curiosity, needs to be settled. The answer here can go either way. On the one hand, although the λσ-calculus [1] does not preserve termination, the σ-calculus itself terminates. On the other hand, could the non-preservation of termination in the λs_e-calculus imply the non-termination of the s_e-calculus?

filtering for uncertain stochastic time-delay systems with sector-bounded nonlinearities

In this paper, we deal with the robust H_∞ filtering problem for a class of uncertain nonlinear time-delay stochastic systems. The system under consideration contains parameter uncertainties, Itô-type stochastic disturbances, time-varying delays, as well as sector-bounded nonlinearities. We aim at designing a full-order filter such that, for all admissible uncertainties, nonlinearities and time delays, the dynamics of the filtering error is guaranteed to be robustly asymptotically stable in the mean square, while achieving the prescribed H_∞ disturbance rejection attenuation level. By using the Lyapunov stability theory and Itô’s differential rule, sufficient conditions are first established to ensure the existence of the desired filters, which are expressed in the form of a linear matrix inequality (LMI). Then, the explicit expression of the desired filter gains is also characterized. Finally, a numerical example is exploited to show the usefulness of the results derived.     

Preface: Volume 86, Issue 3

This volume contains selected papers presented at the International Workshop on Functional and (Constraint) Logic Programming (WFLP 2003), held in Valencia (Spain) during June 12-13, 2003, at the Federated Conference on Rewriting, Deduction and Programming (RDP 2003). WFLP 2003 is the twelfth in the series of international meetings aimed at bringing together researchers interested in functional programming, (constraint) logic programming, as well as their integration. It promotes the cross-fertilizing exchange of ideas and experiences among researches and students from the different communities interested in the foundations, applications, and combinations of high-level, declarative programming languages and related areas. Previous WFLP editions have been held in Grado (Italy), Kiel (Germany), Benicàssim (Spain), Grenoble (France), Bad Honef (Germany), Schwarzenberg (Germany), Marburg (Germany), Rattenberg (Germany), and Karlsruhe (Germany).The Program Committee of WFLP 2003 selected, from all contributions presented at the workshop (which had been reviewed before the workshop), papers for inclusion into this special issue. The authors of all selected papers prepared revised versions after the workshop which were refereed again in order to ensure a high scientific quality. This volume contains the finally accepted versions based on this review process. In addition to the selected papers, the scientific program included invited lectures by Michael Rusinowitch (LORIA-INRIA-Lorraine, France) and Jan Maluszynski (Linköping University, Sweden).The program committee of WFLP 2003 consisted of

María Alpuente	(Technical University of Valencia, Spain)
Sergio Antoy	(Portland State University, USA)
Annalisa Bossi	(Università Ca' Foscari di Venezia, Italy)
Olaf Chitil	(University of York, UK)
Rachid Echahed	(Institut IMAG, France)
Sandro Etalle	(University of Twente, The Netherlands)
Moreno Falaschi	(Università di Udine, Italy)
Michael Hanus	(CAU Kiel, Germany)
Yukiyoshi Kameyama	(University of Tsukuba, Japan)
Herbert Kuchen	(University of Muenster, Germany)
Michael Leuschel	(University of Southampton, UK)
Juan José Moreno-Navarro	(Universidad Politécnica de Madrid, Spain)
Ernesto Pimentel	(University of Málaga, Spain)
Mario Rodríguez-Artalejo	(Universidad Complutense de Madrid, Spain)
Germán Vidal	(Technical University of Valencia, Spain)

Full-size table

Organizing committee: Elvira Albert, Santiago Escobar, César Ferri, José Hernández, Carlos Herrero, Pascual Julián, Marisa Llorens, Ginés Moreno, Javier Oliver, Josep Silva, Germán Vidal, and Alicia VillanuevaAdditional referees: Elvira Albert, Zena Ariola, Demis Ballis, Bernd Brassel, Ricardo Corin, Agostino Dovier, Francisco Durán, Santiago Escobar, José Gallardo, Raffaella Gentilini, Angel Herranz, Teresa Hortalá-González, Zhenjiang Hu, Frank Huch, Pascual Julián, Christoph Lembeck, Pablo López, Salvador Lucas, Massimo Marchiori, Julio Mariño, Yasuhiko Minamide, Angelo Montanari, Ginés Moreno, Roger Müller, Susana Muñoz, Salvatore Orlando, Carla Piazza, Femke van Raamsdonk, María José Ramírez, Guido Sciavicco, Clara Segura, Jan-Georg Smaus, Andrew Tolmach, Alberto Verdejo, and Alicia Villanueva.Sponsoring institutions:Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Generalitat Valenciana, Ministerio de Ciencia y Tecnología, European Association for Theoretical Computer Science, European Association for Programming Languages and Systems, CologNET: A Network of Excellence in Computational Logic, and APPSEM Working Group.I would like to thank the invited speakers for their willingness in accepting our invitation. I would also like to thank all the members of the Program Committee and all the referees for their careful work in the review and selection process. Many sincere thanks to all authors who submitted papers and to all conference participants. I gratefully acknowledge all the institutions and corporations who have supported this workshop. Furthermore, I would like to thank Michael Mislove, Managing Editor of the ENTCS series, for making this special issue possible. Finally, I express my gratitude to all members of the local Organizing Committee whose work has made the workshop possible.November 6, 2003Germán Vidal     

Uniform provability realization of intuitionistic logic, modality and λ-terms

The intended meaning of intuitionistic logic is explained by the Brouwer-Heyting-Kolmogorov (BHK) provability semantics which informally defines intuitionistic truth as provability and specifies the intuitionistic connectives via operations on proofs. The problem of finding an adequate formalization of the provability semantics and establishing the completeness of the intuitionistic logic Int was first raised by Gödel in 1933. This question turned out to be a part of the more general problem of the intended realization for Gödel's modal logic of provability S4 which was open since 1933. In this tutorial talk we present a provability realization of Int and S4 that solves both of these problems. We describe the logic of explicit provability (LP) with the atoms “t is a proof of F” and establish that every theorem of S4 admits a reading in LP as the statement about operations on proofs. Moreover, both S4 and Int are shown to be complete with respect to this realization. In addition, LP subsumes the λ-calculus, modal λ-calculus, combinatory logic and provides a uniform provability realization of modality and λ-terms.     

Design of optimal filters for error-feedback quantization of monochrome pictures

The minimized-average-error bilevel display algorithm of Floyd et al. [1, 2] is extended to a general n-level error-feedback filter for picture display. This filter, which operates recursively on the net system input-output errors using the so-called two-dimensional nonsymmetric half-plane window [3], is analyzed to obtain the optimal properties. Instead of the commonly used distortion measure defined by the pixel-to-pixel mean squared error, a low-pass filter impulse response is used in the spatial domain to define a more reasonable distortion measure based on the concept of error diffusion. Based on the obtained optimal properties of the proposed model, some examples of the design of optimal recursive coefficients utilizing the 2-D IIR filter design technique of Ekstrom et al. [3, 4] are shown.     

The Better Bubbling Lemma

BCD [Barendregt, Henk, Mario Coppo and Mariangiola Dezani-Ciancaglini, A filter lambda model and the completeness of type assignment, JSL 48 (1983), 931–940] relies for its modeling of λ calculus in intersection type filters on a key theorem which I call BL (for the Bubbling Lemma, following someone). This lemma has been extended in [Castagna, Giuseppe, and Alain Frisch. A gentle introduction to semantic subtyping. In PPDP05, ACM Press (full version) and ICALP05, LNCS volume 3580, Springer-Verlag (summary), 2005. Joint ICALP-PPDP keynote talk; Dezani-Ciancaglini, M., A. Frisch, E. Giovannetti and Y. Motohama, 2002. The Relevance of Semantic Subtyping, Electronic Notes in Theoretical Computer Science 70 No. 1, 15pp] to encompass Boolean structure, including specifically union types; this extended lemma I call BBL (the Better Bubbling Lemma). There are resonances, explored in [Dezani-Ciancaglini, M., R.K. Meyer and Y. Motohama, The semantics of entailment omega, NDJFL 43 (2002), 129–145] and [Dezani-Ciancaglini, M., A. Frisch, E. Giovannetti and Y. Motohama, 2002. The Relevance of Semantic Subtyping, Electronic Notes in Theoretical Computer Science 70 No. 1, 15pp], between intersection and union type theories and the already existing minimal positive relevant logic B+ of [Routley, Richard, and Robert K. Meyer, The semantics of entailment III, JPL 1 (1972), 192–208]. (Indeed [Pal, Koushik, and Robert K. Meyer. 2005. Basic relevant theories for combinators at levels I and II, AJL 3, http://www.philosophy.unimelb.edu.au/2005/2003_2.pdf, 19 pages] applies BL and BBL to get further results linking combinators to relevant theories and propositions.) On these resonances the filters of algebra become the theories of logic. The semantics of [Meyer, Robert K., Yoko Motohama and Viviana Bono, Truth translations of relevant logics, in B. Brown and F. Lepage, eds., “Truth and Probability: Essays in Honour of Hugues Leblanc,” pages 59–84, College Publications, King's College, London, 2005] yields here a new and short proof of BBL, which takes account of full Boolean structure by encompassing not only B+ but also its conservative Boolean extension CB [Routley, Richard, and Robert K. Meyer, The semantics of entailment III, JPL 1 (1972), 192–208; Meyer, Robert K., 1995. Types and the Boolean system CB+, cslab.anu.edu.au/ftp/techreports/SRS/1995/TR-SRS-5-95/meyer.ps.gz; Meyer, Robert K., Yoko Motohama and Viviana Bono, Truth translations of relevant logics, in B. Brown and F. Lepage, eds., “Truth and Probability: Essays in Honour of Hugues Leblanc,” pages 59–84, College Publications, King's College, London, 2005.].     

Development of quality bounds for time and frequency domain models: application to the Shell distillation column

Statistical confidence bounds are developed for frequency response and step response models estimated from process input-output data using the frequency sampling filter model structure. The frequency domain bound is an extension of earlier work by the authors (Arifin et al., Journal of Process Control, 1995, 5, 71–76) and the time domain bound is a new result. These bounds provide the engineer with a measure of the quality of the estimated model, and therefore an indication of which aspects of the model are reliable and which aspects require further improvement. The Shell distillation column benchmark problem introduced by Cott (Journal of Process Control, 1995, 5, 60–70) is used for illustrative purposes.     

A Perfect Reconstruction, Size-Limited Filter Bank for Orthogonal, Wavelet-Based, Finite-Signal Subband Processing

Tang, J., and Zhang, Y., A Perfect Reconstruction, Size-Limited Filter Bank for Orthogonal, Wavelet-Based, Finite-Signal Subband Processing, Digital Signal Processing11 (2001) 304–328This paper describes a new scheme to design the size-limited filter banks for orthogonal wavelet-based, finite-signal subband processing. In contrast to the existing schemes based only on boundary extension, our scheme combines boundary extension with boundary filter amendment. The advantages of our scheme lie in that we can guarantee the perfect reconstruction, independence, and orthogonality of the size-limited filter banks.     

A New Delayless Subband Adaptive Filtering Algorithm for Active Noise Control Systems

Subband adaptive filtering (SAF) techniques play a prominent role in designing active noise control (ANC) systems. They reduce the computational complexity of ANC algorithms, particularly, when the acoustic noise is a broadband signal and the system models have long impulse responses. In the commonly used uniform-discrete Fourier transform (DFT) -modulated (UDFTM) filter banks, increasing the number of subbands decreases the computational burden but can introduce excessive distortion, degrading performance of the ANC system. In this paper, we propose a new UDFTM-based adaptive subband filtering method that alleviates the degrading effects of the delay and side-lobe distortion introduced by the prototype filter on the system performance. The delay in filter bank is reduced by prototype filter design and the side-lobe distortion is compensated for by oversampling and appropriate stacking of subband weights. Experimental results show the improvement of performance and computational complexity of the proposed method in comparison to two commonly used subband and block adaptive filtering algorithms.      

Open graphical framework for interactive TV

Multimedia end-user terminals are expected to perform advanced user interface related tasks. These tasks are carried out by user interface runtime tools and include, among others, the visualization of complex graphics and the efficient handling of user input. In addition, the terminal’s graphical system is expected, for example, to be able to synchronize audio and video, and control different contexts on the same screen. Finally, the availability of high-level tools to simplify the user interface implementation and the adaptiveness of the user interfaces for a diversity of configurations are, as well, desirable features. This paper presents a layered model that meets the just mentioned requirements. The architecture is divided into five different layers: hardware abstraction layer, multimedia cross platform libraries, graphical environment, GUI toolkit and high-level languages. Moreover, this paper presents the experiences of developing a prototype system based on the architecture, targeted to digital television receivers. In order to evaluate the prototype, some already developed DVB-MHP compliant digital television applications were tested. Finally, the prototype was extended with a high-level profile (i.e., SMIL support) and a low-level one (i.e., access to the framebuffer memory).

Design of nearly perfect reconstructed non-uniform filter bank by constrained equiripple FIR technique

In this paper, an efficient iterative algorithm is proposed for the design of multi-channel nearly perfect reconstructed non-uniform filter bank. The method employs the constrained equiripple FIR technique to design the prototype filter for filter banks with novelty of exploiting a new perfect reconstruction condition of the non-uniform filter banks instead of using complex objective functions. In the proposed algorithm, passband edge frequency (ω_p) is optimized using linear optimization technique such that the filter coefficients values at quadrature frequency are approximately equal to 0.707. Several design examples are included to illustrate the efficacy of this methodology for designing non-uniform filter bank (NUFB). It was found that the proposed methodology performs better as compared to earlier reported results in terms of reconstruction error (RE), number of iteration (NOI) and computation time (CPU time). The proposed algorithm is very simple, linear in nature, and easy to implement.     

Data Adaptive Linear Decomposition Transform

Cadzow, J. A., and Yammen, S., Data Adaptive Linear Decomposition Transform, Digital Signal Processing12 (2002) 494–523In this paper a novel method for decomposing one-dimensional data sequences is developed. It is of the wavelet variety with important distinctions. A standard wavelet transform entails down-sampling the responses of two fixed structured filters to the sequence being decomposed to produce the half length detail sequence and a coarse sequence. The new transform entails processing down-sampled data by an optimum interpolation filter which seeks to approximate the odd indexed sequence elements by a linear combination of neighboring even indexed elements. The resulting interpolation error sequence of half length plays the role of the wavelet detail sequence. Unlike a traditional wavelet transform, the interpolation filter employed is adapted to the data being analyzed. This data dependency typically produces improved performance relative to traditional wavelet transforms. This enhanced performance is demonstrated on a number of standard test signals. Furthermore, this new transform is computationally efficient due to the inherent parallel structure of the data decomposition method.     

Optimal‐switched extended H∞ filter for nonlinear systems with stochastic uncertainties

The extended H_∞ filter (EH_∞F) is a conservative solution with infinite‐horizon robustness for the state estimation problem regarding nonlinear systems with stochastic uncertainties, which leads to excessive costs in terms of filtering optimality and reduces the estimation precision, particularly when uncertainties related to external disturbances and noise appear intermittently. In order to restore the filtering optimality lost due to the conservativeness of the EH_∞F design, we developed an optimal‐switched (OS) filtering mechanism based on the standard EH_∞F to obtain an optimal‐switched extended H_∞ filter (OS‐EH_∞F). The OS mechanism has an error‐tolerant switched (ETS) structure, which switches the filtering mode between optimal and H_∞ robust by setting a switching threshold with redundancy to uncertainties, and a robustness‐optimality cost function (ROCF) is introduced to determine the threshold and optimize the ETS structure online. The ROCF is the weighted sum of the quantified filtering robustness and optimality. When a weight is given, the proposed OS‐EH_∞F can obtain the optimal state estimates while maintaining the filtering robustness at an invariant ratio. A simulation example of space target tracking has demonstrated the superior estimation performance of the OS‐EH_∞F compared with some other typical filters, thereby verifying the effectiveness of using the weight to evaluate the estimation result of the filters.     

Frequency Domain Frequency Shift for Optimal Filtering of Cyclostationary Signals

Parker, G., Frequency Domain Frequency Shift for Optimal Filtering of Cyclostationary Signals, Digital Signal Processing12 (2002) 561–589Optimum reconstruction of corrupted cyclostationary signals is achieved using the filter class known as the frequency shift filter. This filter requires the received signal to be shifted by the frequencies of cyclostationarity of the signal and with a frequency domain implementation it will often be best to effect the frequency shifts directly in the frequency domain. This paper introduces techniques for exactly achieving these shifts as well as providing more computationally efficient approximate solutions.     

Multiplierless Adaptive Filtering

Bose, T., Venkatachalam, A., and Thamvichai, R., Multiplierless Adaptive Filtering, Digital Signal Processing12 (2002) 107–118When digital filters are designed with power-of-2 coefficients, the multiplications can be implemented by simple shifting operations. For VLSI implementations, multiplierless filters are faster and more compact than filters with multipliers. In this paper, an algorithm for finding and updating the power-of-2 coefficients of an adaptive filter is designed. The new method uses the well-known Genetic Algorithm (GA) for this purpose. The GA is used in a unique way in order to reduce computations. Small blocks of data are used for the GA and only one new generation is produced per sample of data. This, coupled with the fact that the coefficients are power-of-2, yields a computational complexity of O(N) additions and no multiplications. The algorithm is investigated for applications in adaptive linear prediction and system identification. The results are very promising and illustrate the performance of the new algorithm.     

Higher Order Vagueness in Geographical Information: Empirical Geographical Population of Type n Fuzzy Sets

Fuzzy set theory has been suggested as a means for representing vague spatial phenomena, and is widely known for directly addressing some of the issues of vagueness such as the sorites paradox. Higher order vagueness is widely considered a necessary component of any theory of vagueness, but it is not so well known that it too is competently modelled by Type n Fuzzy sets. In this paper we explore the fuzzy representation of higher order vagueness with respect to spatial phenomena. Initially we relate the arguments on philosophical vagueness to Type n Fuzzy sets. As an example, we move on to an empirical generation of spatial Type 2 Fuzzy sets examining the spatial extent of mountain peaks in Scotland. We show that the Type 2 Fuzzy sets can be populated by using alternative parameterisations of a peak detection algorithm. Further ambiguities could also be explored using other parameters of this and other algorithms. We show some novel answers to interrogations of the mountain peaks of Scotland. The conclusion of this work is that higher order vagueness can be populated for Type 2 and higher fuzzy sets. It does not follow that it is always necessary to examine these higher order uncertainties, but a possible advantage in terms of the results of spatial inquiry is demonstrated.

Mobile E-Witness

This paper describes the design, implementation and experimental evaluation of a system prototype, named Mobile E-Witness (MEW), which enables the acquisition and remote storage of multimedia (i.e., audio and video) data streams. In essence, MEW consists of a mobile device, incorporating a camera and a microphone, which can be “worn” (i.e., it can be carried without causing any impediment) by public officers, such as policemen and health care operators, in order to record the events these officers witness while on duty. MEW transmits the audio and video data recordings it takes to a remote storage service which maintains these recordings for future replay. Thus, for example, an event recording can be used as an impartial testimony to resolve disputes concerning the relative responsibilities of those participating to the recorded event, including the officers themselves (hence the name Mobile E-Witness). The infrastructure MEW uses for communications with the remote storage service consists of the wired and wireless communication infrastructures publicly available in metropolitan areas, including the Internet. MEW utilizes these infrastructures in order to (1) ensure that sufficient bandwidth for multimedia data transmission is available, (2) guarantee highly available communications, (3) limit the power consumption for the multimedia transmission and, finally, (4) limit the electromagnetic radiation emanation of the device worn by the public officers. We have carried out an experimental evaluation of a MEW prototype in the city of Bologna. The results of this evaluation, reported in this paper, confirm the potential of our system.

Concrete Process Categories

This paper presents a rather concrete view of a semantic universe for typed concurrent computation. Starting with a notion of sets and functions organized in a category featuring the type theory at hand, we identify the lax slice F//Span ( ) of pseudo-functors from a free category into the bicategory of spans over and triangles commuting up-to a lax natural transformation with representable components as a category of models of concurrency over which the semantic universe unfolds. By analogy, we call the objects of F//Span ( ) categorical transition systems and demonstrate their relevance in giving meaning to a range of everyday phenomena including message passing among imperative programs. We identify the bicategory of spans Span(F//Span ( )) as organizing processes at a basic level and address the question of their equality, articulated as bisimulation w.r.t. actions observable at the interfaces given by the legs of such spans. An appropriate notion of simulation yields a system of open maps by which to quotient Span(F//Span ( )), a construction originally considered by Cockett and Spooner in its generality. The resulting process category Proc(F//Span ( ),) properly contains the well-known interaction category SProc introduced by Abramsky et al.