4 ms·

> there exists a term x that satisfies Ax = B Don't you mean xA = B ? > x can just disregard A and return B Not if you require x to be strict, i.e. it must u

• js8 1y ago
  > Don't you mean xA = B ? No, that equation can be created as a special case from equation TAx = B (where Txy = yx is a transposition combinator). > Not if you require x to be strict, i.e. it must use its argument. I am not sure it would generally help but maybe you mean it only in case of equations xA=B (not Ax=B as I suggested). I also think this strictness condition would be too limiting. In equation Ax=B, we can take A of the form R_n A_1 .. A_n, where R_n reduces Ax to x A_1 .. A_n (R_n rotates x in front of n arguments). So if x is concrete and takes n arguments, we can think of it as "text" (parenthesised expression) in symbols that are to be interpreted as A_1, .. A_n. Requiring that every possible symbol is used in a language text fragment is a weird condition, which doesn't make much sense to me. In any case, my definition of typing judgment then allows to put a chosen condition on a text composed from chosen symbols, which is quite powerful and can be used to e.g. determine whether a quoted expression is valid. And arguably it is a very natural definition in the context of ULC. (I read to Mock a Mockingbird 30 years ago - in partial Slovak translation - and most problems there could be formulated as the Ax=B equation for x being a concrete term.)