scholarly journals Conditional Independence by Typing

2022 ◽  
Vol 44 (1) ◽  
pp. 1-54
Author(s):  
Maria I. Gorinova ◽  
Andrew D. Gordon ◽  
Charles Sutton ◽  
Matthijs Vákár

A central goal of probabilistic programming languages (PPLs) is to separate modelling from inference. However, this goal is hard to achieve in practice. Users are often forced to re-write their models to improve efficiency of inference or meet restrictions imposed by the PPL. Conditional independence (CI) relationships among parameters are a crucial aspect of probabilistic models that capture a qualitative summary of the specified model and can facilitate more efficient inference. We present an information flow type system for probabilistic programming that captures conditional independence (CI) relationships and show that, for a well-typed program in our system, the distribution it implements is guaranteed to have certain CI-relationships. Further, by using type inference, we can statically deduce which CI-properties are present in a specified model. As a practical application, we consider the problem of how to perform inference on models with mixed discrete and continuous parameters. Inference on such models is challenging in many existing PPLs, but can be improved through a workaround, where the discrete parameters are used implicitly , at the expense of manual model re-writing. We present a source-to-source semantics-preserving transformation, which uses our CI-type system to automate this workaround by eliminating the discrete parameters from a probabilistic program. The resulting program can be seen as a hybrid inference algorithm on the original program, where continuous parameters can be drawn using efficient gradient-based inference methods, while the discrete parameters are inferred using variable elimination. We implement our CI-type system and its example application in SlicStan: a compositional variant of Stan. 1

2014 ◽  
Vol 24 (1) ◽  
pp. 56-112 ◽  
Author(s):  
YAN CHEN ◽  
JOSHUA DUNFIELD ◽  
MATTHEW A. HAMMER ◽  
UMUT A. ACAR

AbstractComputational problems that involve dynamic data, such as physics simulations and program development environments, have been an important subject of study in programming languages. Building on this work, recent advances in self-adjusting computation have developed techniques that enable programs to respond automatically and efficiently to dynamic changes in their inputs. Self-adjusting programs have been shown to be efficient for a reasonably broad range of problems, but the approach still requires an explicit programming style, where the programmer must use specific monadic types and primitives to identify, create, and operate on data that can change over time. We describe techniques for automatically translating purely functional programs into self-adjusting programs. In this implicit approach, the programmer need only annotate the (top-level) input types of the programs to be translated. Type inference finds all other types, and a type-directed translation rewrites the source program into an explicitly self-adjusting target program. The type system is related to information-flow type systems and enjoys decidable type inference via constraint solving. We prove that the translation outputs well- typed self-adjusting programs and preserves the source program's input–output behavior, guaranteeing that translated programs respond correctly to all changes to their data. Using a cost semantics, we also prove that the translation preserves the asymptotic complexity of the source program.


2008 ◽  
Vol 18 (4) ◽  
pp. 729-751 ◽  
Author(s):  
ZHAOHUI LUO

We incorporate the idea of coercive subtyping, a theory of abbreviation for dependent type theories, into the polymorphic type system in functional programming languages. The traditional type system with let-polymorphism is extended with argument coercions and function coercions, and a corresponding type inference algorithm is presented and proved to be sound and complete.


2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-28
Author(s):  
Magnus Madsen ◽  
Jaco van de Pol

We present a simple, practical, and expressive relational nullable type system. A relational nullable type system captures whether an expression may evaluate to null based on its type, but also based on the type of other related expressions. The type system extends the Hindley-Milner type system with Boolean constraints, supports parametric polymorphism, and preserves principal types modulo Boolean equivalence. We show how to support full Hindley-Milner style type inference with an extension of Algorithm W. We conduct a preliminary study of open source projects showing that there is a need for relational nullable type systems across a wide range of programming languages. The most important findings from the study are: (i) programmers use programming patterns where the nullability of one expression depends on the nullability of other related expressions, (ii) such invariants are commonly enforced with run-time exceptions, and (iii) reasoning about these programming patterns requires not only knowledge of when an expression may evaluate to null, but also when it may evaluate to a non-null value. We incorporate these observations in the design of the proposed relational nullable type system.


2016 ◽  
Vol 2 ◽  
pp. e55 ◽  
Author(s):  
John Salvatier ◽  
Thomas V. Wiecki ◽  
Christopher Fonnesbeck

Probabilistic programming allows for automatic Bayesian inference on user-defined probabilistic models. Recent advances in Markov chain Monte Carlo (MCMC) sampling allow inference on increasingly complex models. This class of MCMC, known as Hamiltonian Monte Carlo, requires gradient information which is often not readily available. PyMC3 is a new open source probabilistic programming framework written in Python that uses Theano to compute gradients via automatic differentiation as well as compile probabilistic programs on-the-fly to C for increased speed. Contrary to other probabilistic programming languages, PyMC3 allows model specification directly in Python code. The lack of a domain specific language allows for great flexibility and direct interaction with the model. This paper is a tutorial-style introduction to this software package.


Author(s):  
John Salvatier ◽  
Thomas V Wiecki ◽  
Christopher Fonnesbeck

Probabilistic Programming allows for automatic Bayesian inference on user-defined probabilistic models. Recent advances in Markov chain Monte Carlo (MCMC) sampling allow inference on increasingly complex models. This class of MCMC, known as Hamliltonian Monte Carlo, requires gradient information which is often not readily available. PyMC3 is a new open source Probabilistic Programming framework written in Python that uses Theano to compute gradients via automatic differentiation as well as compile probabilistic programs on-the-fly to C for increased speed. Contrary to other Probabilistic Programming languages, PyMC3 allows model specification directly in Python code. The lack of a domain specific language allows for great flexibility and direct interaction with the model. This paper is a tutorial-style introduction to this software package.


Author(s):  
John Salvatier ◽  
Thomas V Wiecki ◽  
Christopher Fonnesbeck

Probabilistic Programming allows for automatic Bayesian inference on user-defined probabilistic models. Recent advances in Markov chain Monte Carlo (MCMC) sampling allow inference on increasingly complex models. This class of MCMC, known as Hamliltonian Monte Carlo, requires gradient information which is often not readily available. PyMC3 is a new open source Probabilistic Programming framework written in Python that uses Theano to compute gradients via automatic differentiation as well as compile probabilistic programs on-the-fly to C for increased speed. Contrary to other Probabilistic Programming languages, PyMC3 allows model specification directly in Python code. The lack of a domain specific language allows for great flexibility and direct interaction with the model. This paper is a tutorial-style introduction to this software package.


2010 ◽  
Vol 39 ◽  
pp. 436-440
Author(s):  
Zhi Ming Qu

In recent years, much research has been devoted to the refinement of IPv6; on the other hand, few have investigated the confusing unification of interrupts and Internet QoS. In this position paper, it demonstrates the emulation of interrupts. In order to overcome this quagmire, a novel system is presented for the intuitive unification of expert systems and massive multiplayer online role-playing games. It is concluded that erasure coding can be verified to make heterogeneous, interposable, and event-driven, which is proved to be applicable.


2013 ◽  
Vol 23 (4) ◽  
pp. 357-401 ◽  
Author(s):  
GEORGES GONTHIER ◽  
BETA ZILIANI ◽  
ALEKSANDAR NANEVSKI ◽  
DEREK DREYER

AbstractMost interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself.We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's canonical structures, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.


2000 ◽  
Vol 11 (01) ◽  
pp. 65-87
Author(s):  
MASATOMO HASHIMOTO

This paper develops an ML-style programming language with first-class contexts i.e. expressions with holes. The crucial operation for contexts is hole-filling. Filling a hole with an expression has the effect of dynamic binding or macro expansion which provides the advanced feature of manipulating open program fragments. Such mechanisms are useful in many systems including distributed/mobile programming and program modules. If we can treat a context as a first-class citizen in a programming language, then we can manipulate open program fragments in a flexible and seamless manner. A possibility of such a programming language was shown by the theory of simply typed context calculus developed by Hashimoto and Ohori. This paper extends the simply typed system of the context calculus to an ML-style polymorphic type system, and gives an operational semantics and a sound and complete type inference algorithm.


Sign in / Sign up

Export Citation Format

Share Document