# The probability of non-confluent systems

@inproceedings{DazCaro2013ThePO, title={The probability of non-confluent systems}, author={Alejandro D{\'i}az-Caro and Gilles Dowek}, booktitle={DCM}, year={2013} }

We show how to provide a structure of probability space to the set of execution traces on a non-confluent abstract rewrite system, by defining a variant of a Lebesgue measure on the space of traces. Then, we show how to use this probability space to transform a non-deterministic calculus into a probabilistic one. We use as example Lambda+, a recently introduced calculus defined through type isomorphisms.

#### 8 Citations

Simply Typed Lambda-Calculus Modulo Type Isomorphisms

- Mathematics, Computer Science
- ArXiv
- 2015

A simply typed, non-deterministic lambda-calculus where isomorphic types are equated and an equivalence relation is settled at the term level is defined and a proof of strong normalisation modulo equivalence is provided. Expand

The vectorial λ-calculus

- Computer Science, Mathematics
- Inf. Comput.
- 2017

It is proved that the resulting typed λ-calculus is strongly normalising and features weak subject reduction and it is shown how to naturally encode matrices and vectors in this typed calculus. Expand

The Vectorial Lambda-Calculus

- Computer Science
- ArXiv
- 2013

It is proved that the resulting typed lambda-calculus is strongly normalising and features a weak subject reduction and it is shown how to naturally encode matrices and vectors in this typed calculus. Expand

L O ] 5 A ug 2 01 3 The Vectorial Lambda-Calculus

- 2014

We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the linear-algebraic aspects of this extension of lambda-calculus: it is able to statically describe… Expand

Functional Pearl: The Distributive $\lambda$-Calculus

- Computer Science, Mathematics
- 2020

It is shown that the new rules of the distributive $\lambda$-calculus with pairs satisfy subject reduction if types are considered up to the distributivity isomorphism, and that the main result is strong normalization for simple types up to distributivity. Expand

Functional and Logic Programming: 15th International Symposium, FLOPS 2020, Akita, Japan, September 14–16, 2020, Proceedings

- Computer Science
- FLOPS
- 2020

The fundamental determinants of poor performance scaling by Coq’s proof engine are studied, and preliminary results on bottlenecks in key operations are sketches. Expand

Fe b 20 20 Functional Pearl : The Distributive λ-Calculus

- 2020

Functional Pearl: The Distributive λ-Calculus

- Computer Science, Mathematics
- FLOPS
- 2020

A simple extension of the \(\lambda \)-calculus with pairs with pairs is introduced by adding a computational interpretation of the valid distributivity isomorphism \(A \Rightarrow (B\wedge C) \equiv (A\Rightarrow B) \wedge (A}\Rightarrow C) of simple types. Expand

#### References

SHOWING 1-10 OF 37 REFERENCES

Normalisation of a Non-deterministic Type Isomorphic {\lambda}-calculus

- Mathematics, Computer Science
- 2013

We provide a proof of strong normalisation for lambda+, a recently introduced, explicitly typed, non-deterministic lambda-calculus where isomorphic propositions are identified. Such a proof is a… Expand

Probabilistic /lambda-calculus and Quantitative Program Analysis

- Computer Science
- J. Log. Comput.
- 2005

It is shown how the framework of probabilistic abstract interpretation can be applied to statically analyse a Probabilistic version of the λ-calculus to allow for a more speculative use of its outcomes based on the consideration of statistically defined quantities. Expand

Probabilistic λ-calculus and Quantitative Program Analysis

- 2004

We show how the framework of probabilistic abstract interpretation can be applied to statically analyse a probabilistic version of the λ-calculus. The resulting analysis allows for a more speculative… Expand

The algebraic lambda calculus

- Computer Science, Mathematics
- Mathematical Structures in Computer Science
- 2009

An extension of the pure lambda calculus is introduced by endowing the set of terms with the structure of a vector space, or, more generally, of a module, over a fixed set of scalars, and it is proved it is confluent. Expand

Linearity in the Non-deterministic Call-by-Value Setting

- Mathematics, Computer Science
- WoLLIC
- 2012

A fine-grained type system is defined, capturing the right linearity present in such formalisms as the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. Expand

Non determinism through type isomorphism

- Mathematics, Computer Science
- LSFA
- 2012

An equivalence relation on propositions and a proof system where equivalent propositions have the same proofs are defined, which resembles several known non-deterministic and algebraic lambda-calculi. Expand

Rewriting Logic and Probabilities

- Computer Science, Mathematics
- RTA
- 2003

Whether there exists a notion of probabilistic rewrite system with an associated notion of Probabilistic rewriting logic is discussed. Expand

Call-by-Value Non-determinism in a Linear Logic Type Discipline

- Computer Science, Mathematics
- LFCS
- 2013

It is proved that a term is typable if and only if it is converging, and that its typing tree carries enough information to give a bound on the length of its lazy call-by-value reduction. Expand

A relational semantics for parallelism and non-determinism in a functional setting

- Mathematics, Computer Science
- Ann. Pure Appl. Log.
- 2012

This paper introduces a λ -calculus extended with non-deterministic choice and parallel composition and defines its operational semantics (based on the may and must intuitions underlying the authors' two additional operations), and describes the interpretation of this calculus in this model. Expand

Process Algebra with Probabilistic Choice

- Computer Science
- ARTS
- 1999

This paper treats the problem of combining parallel composition with probability and with or without non-determinism in the setting of process algebra in the form of ACP to obtain the Basic Process Algebra with probabilistic choice prBPA and the axiom system for ACP+π. Expand