A Common Mathematical Framework for Asymptotic Complexity Analysis and Denotational Semantics for Recursive Programs Based on Complexity Spaces

This paper describes the Automated Complexity Analysis Prototype (ACAp) system for automated complexity analysis of functional programs synthesized with the Nuprl proof development system. We define a simple abstract cost model for NUPRL's term language based on the current call-by-name evaluator. The framework uses abstract functions and abstract lists to facilitate reasoning about primitive recursive programs with first-order functions, lazy lists and a subclass of higher-order functions. The ACAp system automatically derives upper bounds on the time complexity of NUPRL extracts relative to a given profiling semantics. Analysis proceeds by abstract interpretation of the extract, where symbolic evaluation rules extend standard evaluation to terms with free variables. Symbolic evaluation of recursive programs generates systems of multi-variable difference equations, which are solved using the MATHEMATICA computer algebra system. The use of the system is exemplified by analyzing a proof extract that computes the maximum segment sum of a list and a functional program that determines the minimum of a list via sorting. For both results, we compare call-by-name to call-by-value evaluation.

Download Full-text

Parameter Learning of Logic Programs for Symbolic-Statistical Modeling

Journal of Artificial Intelligence Research ◽

10.1613/jair.912 ◽

2001 ◽

Vol 15 ◽

pp. 391-454 ◽

Cited By ~ 102

Author(s):

T. Sato ◽

Y. Kameya

Keyword(s):

Em Algorithm ◽

Bayesian Networks ◽

Complexity Analysis ◽

Statistical Parameter ◽

Research Field ◽

Mathematical Framework ◽

Parameter Learning ◽

Sequential Decision ◽

Logic Programs ◽

Possible World

We propose a logical/mathematical framework for statistical parameter learning of parameterized logic programs, i.e. definite clause programs containing probabilistic facts with a parameterized distribution. It extends the traditional least Herbrand model semantics in logic programming to distribution semantics, possible world semantics with a probability distribution which is unconditionally applicable to arbitrary logic programs including ones for HMMs, PCFGs and Bayesian networks. We also propose a new EM algorithm, the graphical EM algorithm, that runs for a class of parameterized logic programs representing sequential decision processes where each decision is exclusive and independent. It runs on a new data structure called support graphs describing the logical relationship between observations and their explanations, and learns parameters by computing inside and outside probability generalized for logic programs. The complexity analysis shows that when combined with OLDT search for all explanations for observations, the graphical EM algorithm, despite its generality, has the same time complexity as existing EM algorithms, i.e. the Baum-Welch algorithm for HMMs, the Inside-Outside algorithm for PCFGs, and the one for singly connected Bayesian networks that have been developed independently in each research field. Learning experiments with PCFGs using two corpora of moderate size indicate that the graphical EM algorithm can significantly outperform the Inside-Outside algorithm.

Download Full-text

Nonstandard logics of recursive programs and denotational semantics

Algebraic and Logic Programming - Lecture Notes in Computer Science ◽

10.1007/3-540-50667-5_78 ◽

1988 ◽

pp. 255-278

Author(s):

Ana Pasztor

Keyword(s):

Denotational Semantics ◽

Recursive Programs

Download Full-text

Profunctors, Open Maps and Bisimulation

BRICS Report Series ◽

10.7146/brics.v11i22.21847 ◽

2004 ◽

Vol 11 (22) ◽

Cited By ~ 7

Author(s):

Gian Luca Cattani ◽

Glynn Winskel

Keyword(s):

Programming Languages ◽

Linear Logic ◽

Denotational Semantics ◽

Mathematical Framework ◽

General Applicability ◽

Semantics Of Programming Languages ◽

Open Map ◽

Linear Maps ◽

Concurrent Computation ◽

Open Maps

This paper studies fundamental connections between profunctors (i.e., distributors, or bimodules), open maps and bisimulation. In particular, it proves that a colimit preserving functor between presheaf categories (corresponding to a profunctor) preserves open maps and open map bisimulation. Consequently, the composition of profunctors preserves open maps as 2-cells. A guiding idea is the view that profunctors, and colimit preserving functors, are linear maps in a model of classical linear logic. But profunctors, and colimit preserving functors, as linear maps, are too restrictive for many applications. This leads to a study of a range of pseudo-comonads and how non-linear maps in their co-Kleisli bicategories preserve open maps and bisimulation. The pseudo-comonads considered are based on finite colimit completion, ``lifting'', and indexed families. The paper includes an appendix summarising the key results on coends, left Kan extensions and the preservation of colimits. One motivation for this work is that it provides a mathematical framework for extending domain theory and denotational semantics of programming languages to the more intricate models, languages and equivalences found in concurrent computation. But the results are likely to have more general applicability because of the ubiquitous nature of profunctors.

Download Full-text