Post Correspondence Problem

I found out that one of topics on my final exam will be Post Correspondence Problem. Definition of this problem is pretty straightforward. I am not going to write down formal definition, since it is available on Internet.
You have given two lists A = (a₁, a₂, a₃,...) and B = (b₁, b₂, b₃,...) with same number of items. Each list contains strings. The task is to determine if exists sequence of indexes -- integers i₁, i₂, i₃,... such that a_i1, a_i2, a_i3,... = b_i1, b_i2, b_i3,....

Example

A = (abb, a, bab)
B = (bba, aab, b)

So our task is to make one word with one list of indexes using A and B.
In the first step we have to pick wisely, because we might end pretty early. Using index 1 would be a bad choice because abb and bba can't be prefix of the same word. Indexes 2 and 3 are far better choices. Let's say I pick 2. So our word looks like this right now:

A: a
B: aab

It's easy to see, that we have to find string with prefix ab in list A. We are lucky! Index number 1 fulfills our condition:

A: aabb
B: aabbba

Similar situation, but prefix to be found is ba in A. Index 3 fits:

A: aabbbab
B: aabbbab

Both strings match, we have found a solution: (2, 1, 3).

Programming

I couldn't understand, how come that this problem is undecidable (I haven't read proof proving undecidability). So I tried to program it using python. Basicly the problem could be seen as a graph problem (from the brute force perspective) -- searching for correct path in a tree. Actual code might be buggy since I didn't test it much:

def returnSuffix(a, b):
 result = ''
 aLen = len(a)
 bLen = len(b)
 if aLen > bLen:
  if a[:len(b)] == b:
   return a[len(b):]
  else:
   return None
 else:
  if b[:len(a)] == a:
   return b[len(a):]
  else:
   return None

def getStr(a):
 return ''.join([''.join(v[1]) for v in a]) 

a = ['bba', 'abb', 'bb', 'a']
b = ['bb', 'b', 'abba', 'ba']

depth = 0 
aString = []
bString = []
indexes = []
choices = []
firstRun = True
found = False

while firstRun or len(choices) > 0 or len(aString): 
 firstRun = False 
 deadEnd = True 
 #pdb.set_trace()
 for idx, val in enumerate(a):
  if returnSuffix(getStr(aString) + val, getStr(bString) + b[idx]) != None:
   print 'adding %d to choices' % idx
   choices.append([depth, idx])
   deadEnd = False
 print 'choices: %s' % choices
 if not deadEnd:
  lastItem = choices.pop() 
  indexes.append(lastItem[1])
  aString.append([lastItem[0], a[lastItem[1]]])
  bString.append([lastItem[0], b[lastItem[1]]])
  if (getStr(aString) == getStr(bString)):
   print 'Solution found! %s' % indexes
   found = True   
   break
  depth = lastItem[0] + 1
  print getStr(aString)
  print getStr(bString)
 elif len(choices) == 0:
  break;   
 elif deadEnd:
  if (aString[-1][0] == 0):
   aString.pop()
   bString.pop()
   indexes.pop()
  else:   
   while choices[-1][0] <= aString[-1][0]:
    aString.pop()
    bString.pop()
    indexes.pop()
    depth = depth - 1
  if len(choices) > 0:
   lastItem = choices.pop()   
   indexes.append(lastItem[1])
   aString.append([lastItem[0], a[lastItem[1]]])
   bString.append([lastItem[0], b[lastItem[1]]])
   depth = lastItem[0] + 1
 if depth > 10:
  print 'depth is bigger than 10'
  break;
if not found:
 print 'Solution not found'

So what does this code do? Variables aString and bString represents actual path in a tree, while variable choices contains pointers to alternative branches. Variable depth represents the level in a tree. Function getStr just returns the actual state of building the string. Function returnSuffix returns suffix of word built from a which differs from b and vice versa. If the two words are invalid, it returns None.
And now the actual algorithm. For current vertex program computes all the branches and add them to choices. If the branch is dead end, it will return back to the last crossroad and tries alternative branch. If it's not, it pops last item from choices and continues. So basically it's Depth-first search. The only problem is that we are not searching one tree, but more of them. These are specified as depth=0 items in choices. So if you walk whole tree there has to be different routine to jump to another three -- if (aString[-1][0] == 0):.
So why is the problem undecidable? Because the tree may contain infinite paths and there is no way out how to decide whether the path is infinite or just "too long" -- depth variable. That's the exact definition of undecidability:
A problem is undecidable if it cannot be solved by any Turing machine that halts on all inputs.