I needed a refresher about church encoding myself so I'll add a clarification for other users:
Church encoding essentially defines numbers using 0 and a "next function". E.g. 1 is next(0) and 4 is next(next(next(next(0)))).
Division of church-encoded numbers comes down to repeatedly subtracting the divisor from the dividend until you get a number that is smaller than the divisor, then counting how many iterations you've had.
With this kind of division, dividing by 0 results in an infinite loop. Although we cannot evaluate this, we could 'cache' the value of division by 0 to infinity.
Back to the Curry-Howard isomorphism: as I briefly mentioned, under infinite recursion, the type system does not constitute a proof, so again, you could say that, even for church-encoded numbers, we do not have any proof for division by 0, ergo it should not be in the type system.
On the other hand, you might say that the proof system for weak functional programming (which is what we generally refer to as function programming) is simply not sound (i.e. wrong), and allows for infinite recursion as a 'proof', in which case dividing a church-encoded number by 0 results in infinity.
It really boils down to the context and the problem, any recursive definition could potentially be infinite recursive. Our best bet is always keeping the domain in check for the said problem and evaluating our proof. Also, even in formal math proofs a lot of things are just skipped over and considered a given. Division by zero is one of those.
Though, integer representation is a pretty fluid problem, in that there can be more than one representations that get the job done. So, when using lambda calculus or purely functional programming as a basis for proof one could argue that there may exist a better representation.
For further actions, you may consider blocking this person and/or reporting abuse
We're a place where coders share, stay up-to-date and grow their careers.
If we go by a recursive division implementation, we get an infinite recursion. That should be expected :-P
I needed a refresher about church encoding myself so I'll add a clarification for other users:
Church encoding essentially defines numbers using 0 and a "
nextfunction". E.g. 1 isnext(0)and 4 isnext(next(next(next(0)))).Division of church-encoded numbers comes down to repeatedly subtracting the divisor from the dividend until you get a number that is smaller than the divisor, then counting how many iterations you've had.
With this kind of division, dividing by 0 results in an infinite loop. Although we cannot evaluate this, we could 'cache' the value of division by 0 to infinity.
Back to the Curry-Howard isomorphism: as I briefly mentioned, under infinite recursion, the type system does not constitute a proof, so again, you could say that, even for church-encoded numbers, we do not have any proof for division by 0, ergo it should not be in the type system.
On the other hand, you might say that the proof system for weak functional programming (which is what we generally refer to as function programming) is simply not sound (i.e. wrong), and allows for infinite recursion as a 'proof', in which case dividing a church-encoded number by 0 results in infinity.
It really boils down to the context and the problem, any recursive definition could potentially be infinite recursive. Our best bet is always keeping the domain in check for the said problem and evaluating our proof. Also, even in formal math proofs a lot of things are just skipped over and considered a given. Division by zero is one of those.
Though, integer representation is a pretty fluid problem, in that there can be more than one representations that get the job done. So, when using lambda calculus or purely functional programming as a basis for proof one could argue that there may exist a better representation.