Skip to main content
Software Engineering

Return to Answer

added 183 characters in body
Source Link
user7043
user7043

It is indeed impossible to determine semantic equivalence of lambda calculus terms. This is one application of Rice's theorem. However, it's easy to compare terms syntactically, that is, test if they have the exact same structure (equivalently, if their "string representation" is the same). That's really all you need to get results.

For example, to compute functions n = f(i) from the naturals to the naturals, you supply the church encoding of i as parameter to your lambda calculus function, apply reduction rules until you come to a stop, and inspect the resulting term. If it matches the structure of church numerals, extract the number n which it encodes. That's your result. If If the resulting term doesn't look like a church numeral, or reduction doesn't halt, the function is undefined at i. Lambda calculus terms

Terms effectively pull double duty as code"code" and data"data". Likewise, aThat's nothing special: A Turing machine's tape (a string over some alphabet) can also be --- and frequently is --- interpreted as an encoding of a Turing machine or of some aspect thereof. Likewise, the bits in a von Neumann machine's main memory can be either an encoding of a program or an encoding of something else. Or even both at once. It's only the "default perspective" that differs.

It is indeed impossible to determine semantic equivalence of lambda calculus terms. This is one application of Rice's theorem. However, it's easy to compare terms syntactically, that is, test if they have the exact same structure (equivalently, if their "string representation" is the same). That's really all you need to get results.

For example, to compute functions n = f(i) from the naturals to the naturals, you supply the church encoding of i as parameter to your lambda calculus function, apply reduction rules until you come to a stop, and inspect the resulting term. If it matches the structure of church numerals, extract the number n which it encodes. That's your result. If the resulting term doesn't look like a church numeral, or reduction doesn't halt, the function is undefined at i. Lambda calculus terms effectively pull double duty as code and data. Likewise, a Turing machine's tape (a string over some alphabet) can also be interpreted as an encoding of a Turing machine or some aspect thereof. It's only the "default perspective" that differs.

It is indeed impossible to determine semantic equivalence of lambda calculus terms. This is one application of Rice's theorem. However, it's easy to compare terms syntactically, that is, test if they have the exact same structure (equivalently, if their "string representation" is the same). That's really all you need to get results.

For example, to compute functions n = f(i) from the naturals to the naturals, you supply the church encoding of i as parameter to your lambda calculus function, apply reduction rules until you come to a stop, and inspect the resulting term. If it matches the structure of church numerals, extract the number n which it encodes. That's your result. If the resulting term doesn't look like a church numeral, or reduction doesn't halt, the function is undefined at i.

Terms effectively pull double duty as "code" and "data". That's nothing special: A Turing machine's tape (a string over some alphabet) can be --- and frequently is --- interpreted as an encoding of a Turing machine or of some aspect thereof. Likewise, the bits in a von Neumann machine's main memory can be either an encoding of a program or an encoding of something else. Or even both at once. It's only the "default perspective" that differs.

Source Link
user7043
user7043

It is indeed impossible to determine semantic equivalence of lambda calculus terms. This is one application of Rice's theorem. However, it's easy to compare terms syntactically, that is, test if they have the exact same structure (equivalently, if their "string representation" is the same). That's really all you need to get results.

For example, to compute functions n = f(i) from the naturals to the naturals, you supply the church encoding of i as parameter to your lambda calculus function, apply reduction rules until you come to a stop, and inspect the resulting term. If it matches the structure of church numerals, extract the number n which it encodes. That's your result. If the resulting term doesn't look like a church numeral, or reduction doesn't halt, the function is undefined at i. Lambda calculus terms effectively pull double duty as code and data. Likewise, a Turing machine's tape (a string over some alphabet) can also be interpreted as an encoding of a Turing machine or some aspect thereof. It's only the "default perspective" that differs.