I think that the problem is in the way you define the prior. Here is an alternative proposal:
Given a lambda-term t, we can interpret it as defining a partial function ft:{0,1}∗×{0,1}×N⇀Q∩[0,1]. This function works by applying t to the (appropriately encoded) inputs, beta-reducing, and then interpreting the result as an element of Q∩[0,1] using some reasonable encoding. It’s a partial function because the reduction can fail to terminate or the output can violate the expected format.
Given f:{0,1}∗×{0,1}×N⇀Q∩[0,1], we define the “corrected” function ^f:{0,1}∗×{0,1}×N⇀Q∩[0,1] as follows. (The goal here is to make it monotonic in the last argument, and also ensure that probabilities sum to ≤1.) First, we write fmax(u,b,k)=x whenever (i) for all i≤k, (u,b,i)∈dom(f) and (ii) x=maxi≤kf(u,b,i). If there is no such x (i.e. when condition i fails) then fmax(u,b,k) is undefined. Now, we have two cases:
When ∀i≤k:fmax(u,0,i)+fmax(u,1,i)≤1 (in particular, the terms on the LHS are defined), we define ^f(u,b,k):=fmax(u,b,k).
In other cases, we define ^f(u,b,k):=fmax(u,b,j) where j is maximal s.t.(u,b,j) is in the former case. If there is no such j, we set ^f(u,b,k):=0.
We can now define the semimeasure μf by
μf(b|u):=limk→∞^f(u,b,k)
For f=ft, this semimeasure is lower-semicomputable. Conversely, any lower-semicomputable semimeasure is of this form. Mixing these semimeasures according to our prior over lambda terms gives the desired Solomonoff-like prior.
I think that the problem is in the way you define the prior. Here is an alternative proposal:
Given a lambda-term t, we can interpret it as defining a partial function ft:{0,1}∗×{0,1}×N⇀Q∩[0,1]. This function works by applying t to the (appropriately encoded) inputs, beta-reducing, and then interpreting the result as an element of Q∩[0,1] using some reasonable encoding. It’s a partial function because the reduction can fail to terminate or the output can violate the expected format.
Given f:{0,1}∗×{0,1}×N⇀Q∩[0,1], we define the “corrected” function ^f:{0,1}∗×{0,1}×N⇀Q∩[0,1] as follows. (The goal here is to make it monotonic in the last argument, and also ensure that probabilities sum to ≤1.) First, we write fmax(u,b,k)=x whenever (i) for all i≤k, (u,b,i)∈dom(f) and (ii) x=maxi≤kf(u,b,i). If there is no such x (i.e. when condition i fails) then fmax(u,b,k) is undefined. Now, we have two cases:
When ∀i≤k:fmax(u,0,i)+fmax(u,1,i)≤1 (in particular, the terms on the LHS are defined), we define ^f(u,b,k):=fmax(u,b,k).
In other cases, we define ^f(u,b,k):=fmax(u,b,j) where j is maximal s.t.(u,b,j) is in the former case. If there is no such j, we set ^f(u,b,k):=0.
We can now define the semimeasure μf by
μf(b|u):=limk→∞^f(u,b,k)For f=ft, this semimeasure is lower-semicomputable. Conversely, any lower-semicomputable semimeasure is of this form. Mixing these semimeasures according to our prior over lambda terms gives the desired Solomonoff-like prior.