• V.Danos, M.Pedicini, L.Regnier Directed Virtual Reductions, In M.Bezem D.van Dalen, editor, Computer Science Logic, 10th  International Workshop, CSL '96, volume 1258 of Lecture Notes in Computer Science, pages 76--88. EACSL, Springer Verlag, 1997. [format postscript or gzipped postscript].

ABSTRACT: This note defines a new graphical local calculus, \emph{directed virtual reductions}. It is designed to compute Girard's execution formula \EX, an invariant of closed functional evaluation obtained from the ``geometry of interaction'' interpretation of $\lambda$-calculus \cite{Girard88a}. The calculus is obtained by synchronizing another graphical local calculus presented in ``local and asynchronous beta-reduction'': \emph{virtual reductions} \cite{DanosRegnier93}. This synchronization makes it easier to mechanize than general virtual reductions. In undirected virtual reductions the consistency of the computation is insured by an algebraic mechanism called the \emph{bar}. This mechanism in general induces correction terms of any order. The directed virtual reduction has been designed to keep those terms at order one. A further synchronization, the \emph{combustion strategy} will even wipe out first order correction terms. Applied to sharing graphs, the combustion strategy yields Lamping's optimal graphical calculus as presented in \cite{AbadiGonthierLevy92a}. But more efficient optimal implementations of $\lambda$-calculus are expected. The paper is conceived as a follow-up of \cite{DanosRegnier93} and supposes a familiarity with virtual reduction.

 

• P.Loreti, M.Pedicini, An Idempotent Analogue of Resolvent Kernels for a Deterministic Optimal Control Problem Technical Report IAC n.16 1996. [format gzipped postscript].

ABSTRACT: In this paper we investigate the discretized Hamilton-Jacobi-Bellman equation by formulating it in the idempotent semiring of real numbers with operations min and +. It results to be the idempotent analogue of the Volterra integral equation of second type and it can be approximated by the method of the resolvent kernel.

 

• M.Pedicini, Remarks on Elementary Linear Logic, in Electronic Notes in Theoretical Computer Science Volume 3, A Special Issue on the "Linear Logic 96, Tokyo Meeting" [format postscript].

ABSTRACT: Last works in linear logic mark a trend that can be summarized as: studying of fragments of calculi which have good logical properties and a quite powerful class of representable functions. ELL is a system derived from linear logic which presents several of such good properties: first of all a bound of the cut-elimination procedure which is lower w.r.t. the usual one.

 

• F.Costantini, G.F.Mascari, M.Pedicini, Dynamics of Algorithms Technical Report IAC n.6 1996 [format gzipped postscript].

ABSTRACT: A challenge problem in studying complex systems is to model internal structure of the system and its dynamical evolution in an integrated view. An algorithm computes a function with domain consisting of all its possible inputs and as codomain all possible outputs. In order to ''compare'' algorithms computing the same function (e.g. with respect to time or space complexity) it is necessary to model the ''dynamic behavior'' of the algorithm. The main approach for modeling the dynamic behavior $Bh({\bf P})$ of an algorithm is ''the dynamic system paradigm'': $Bh({\bf P})$ is obtained as the action of a (control) monoid on a (state) space. Various mathematical structures have been considered for attacking such a problem; among others, deterministic automata and stochastic automata. In order to capture the fine structure of computation, recently an attempt to describe the ''macroscopic'' global dynamic behavior of an algorithm in terms of the ''microscopic'' local dynamic behavior of its components has been proposed within a logical approach to computing called ''Geometry of Interaction'' developed within $C^{*}$-algebras. We propose an algebraic approach to ``structured dynamics'' inspired by the Geometry of Interaction and based on a ''many objects'' generalization of semirings: partially additive categories.

 

• M.Pedicini, G.Pontrelli, Symbolic Calculus in Non-Newtonian Fluid Mechanics Technical Report IAC n.4 1996.

ABSTRACT: A general purpose package in Mathematica environment for the automatic computation of non-newtonian flow equations is developed and presented. The software allows the user to chose among three coordinate systems and four different fluid models. Changing of variables, scaling and other formal manipulation of the equations are also possible.

 

• G. F. Mascari, M. Pedicini, Types and Dynamics in Partially Additive Categories , in "Idempotency" , Ed. J.Gunawardena, Publications of the Isaac Newton Institute, vol. 11. Cambridge University Press (1998).

ABSTRACT: In this paper we present a general view of structural dynamics inspired by proof theory. The execution of pseudoalgorithms defined in the framework of partially additive categories is given as a kind of iteration of endomorphisms. We also consider deadlock free pseudoalgorithms as to be characterized by a summability condition and the theorem stating modularity with respect to dynamics is proved. Finally in the last section, concepts about structural aspects are organized via type discipline and type compatible dynamics.

 

• G.F. Mascari,M.Pedicini, Head Linear Reduction and Pure Proof Net Extraction, in TCS 135 (1994) 111-137.

ABSTRACT: Proof net calculus introduced in [Gir86] has been extended in the paradigm of the Scott's domains equation D = D -> D which generates a logical point of view for pure lambda-calculus in [Dan89]. Methodologically speaking: in this paper the proof theoretic counterpart of the Böhm's Theorem given in [Boh68] for pure lambda-calculus, is proposed as extention of the Curry-Howard paradigm. Tecnically speaking: as the extraction of a subterm using the beta-reduction is possible also subnet extraction can be internalized by cut-elimination: using proof nets helps us to understand more deeply, and to handle in a better way the procedure of extraction.

 

• M.Pedicini, Schémas Principaux et Réseaux de Preuves, Memoire de DEA, Univ. Paris VII.

ABSTRACT: Dans [Gir86] on peut trouver la definition des reseaux pour la logique lineaire, Vincent Danos et Laurent Regnier [Dan89] ont montre comment on peut traduire le lambda calcul pur dans un cas particulier des reseaux du fragment multiplicatif avec exponentielles (notamment la ou on voit que il n'y a que les formules I,O,!I,?O a cause de l'equation au point fixe D=D -> D du lambda-calcul pur et des lois de De Morgan valides pour les connecteures de la logique lineaire). Ici on introduit un formalisme different pour les reseaux normaux et on demontre que ces reseaux correspondent aux types principaux dans le systeme D(Omega). Les resultats contenus dans ce memoire sont dus au travail de Jacques Van de Wiele et Eric Duquesne.