Probabilistic Constructions of Computable Objects and a Computable Version of Lov\'asz Local Lemma

TL;DR

This paper explores how probabilistic existence proofs, specifically a computable version of the Lovász local lemma, can be adapted to construct computable infinite objects, including a survey of related probabilistic methods.

Contribution

It introduces a method to derive computable objects from probabilistic proofs using layerwise computable mappings, extending the Lovász local lemma to the computable setting.

Findings

Develops a computable version of Lovász local lemma

Uses layerwise computable mappings for construction

Includes a survey of Moser-Tardos proof techniques

Abstract

A nonconstructive proof can be used to prove the existence of an object with some properties without providing an explicit example of such an object. A special case is a probabilistic proof where we show that an object with required properties appears with some positive probability in some random process. Can we use such arguments to prove the existence of a computable infinite object? Sometimes yes: following [8], we show how the notion of a layerwise computable mapping can be used to prove a computable version of Lov\'asz local lemma. (A survey of Moser-Tardos proof is included to make the paper self-contained.)