It would be interesting to see someone like Tromp explore binary FOL the way he's explored binary lambda calculus*. There are good reasons for going the FOL direction since functions are degenerate relations. While it is true that functional languages based on, for example, lambda or SK calculus, can naturally support "and parallelism" (eg x^2 in parallel with y^2 in x^2+y^2), getting "or parallelism" requires expression of independent processes (e.g.indeterminacy), some of which may not terminate. For example, operating systems need "or parallelism".
*I'm not at all comfortable with Tromp's abandoning SK for lambda calculus in his search for a principled choice of UTM for Algorithmic Information Theory. His justification seems to be that lambda is "more expressive" than sk, but that begs the question: To express _what_?
Comments
It would be interesting to see someone like Tromp explore binary FOL the way he's explored binary lambda calculus*. There are good reasons for going the FOL direction since functions are degenerate relations. While it is true that functional languages based on, for example, lambda or SK calculus, can naturally support "and parallelism" (eg x^2 in parallel with y^2 in x^2+y^2), getting "or parallelism" requires expression of independent processes (e.g.indeterminacy), some of which may not terminate. For example, operating systems need "or parallelism".
*I'm not at all comfortable with Tromp's abandoning SK for lambda calculus in his search for a principled choice of UTM for Algorithmic Information Theory. His justification seems to be that lambda is "more expressive" than sk, but that begs the question: To express _what_?