# One-Dimensional Random Walk A particle starts at position x = 10 and moves with equal probability one unit to the left or one unit to the right in each turn. The random walk stops if the particle reaches position x = 0. The walk terminates with probability one [2] but requires, on average, an infinite time to do so [1], i.e., the expected number of turns is infinite. How many turns does a walk take?

mc_sample_arg_first(walk(T),1,T,[NT-_]).

## Code Preamble:

:- use_module(library(mcintyre)). :- if(current_predicate(use_rendering/1)). :- use_rendering(c3). :- endif. :- mc. :- begin_lpad.

The walk starts at time=0 and X=0.

walk(T):- walk(10,0,T).

If X is 0, the walk ends.

walk(0,T,T).

If X>0, the particle makes a move.

walk(X,T0,T):- X>0, move(T0,Move), T1 is T0+1, X1 is X+Move, walk(X1,T1,T).

The move is either one step to the left or to the right with equal probability.

move(T,1):0.5; move(T,-1):0.5.

Epilogue:

:-end_lpad.

## References [1] Kaminski, B. L., Katoen, J.-P., Matheja, C., Olmedo, F., Weakest precondition reasoning for expected run-times of probabilistic programs. Programming languages and systems, LNCS, vol. 9632, pp. 364-389, Springer, Heidelberg (2016) [2] Hurd, J.: A formal approach to probabilistic termination. In: Carreno, V.A., Munoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 230-245, Springer, Heidelberg (2002)