It is well-known that the question whether a given connected simplicial complex (or simplicial set) is simply connected, is algorithmically undecidable as it can model the word problem.

Assuming that $X$ is simply connected, is there an algorithmic way how to contract loops?

One way how this can be formalized is as follows. $X$ can be a simply connected simplicial set (with either finitely many nondegenerate simplices in each dimension, or at least with effective homology...) and $\tilde{GX}$ the Kan model of the loop space, such as described here. The loop contraction would than be a map $c: \tilde{GX}_0\to \tilde{GX}_1$ such that $d_0 c(x)=x$ and $d_1 c(x)=1$. Is there any hope to have a general algorithm for evaluating $c(x)$?