The consequences of not being able to add natural numbers to C

Question

In system F, I can define a true summation function using numerals.

In Haskell, I cannot define this function due to a lower value. For example, in haskell, if x + y = x, then I cannot say that y is zero, if x is the bottom, x + y = x for any y. Thus, the addition is not a true addition, but an approximation to it.

In C, I cannot define this function because the C specification requires that everything has a finite size. Thus, in C, possible approximations are even worse than in Haskell.

So we have:

In System F, add-ons can be defined, but it is not possible to have a complete implementation (since there is no endless hardware).

In Haskell, it is not possible to define an addition (due to the bottom), and it is not possible to complete the implementation.

In C, it is impossible to define the complete addition function (since the semantics of everything are limited), but compatible implementations are possible.

Thus, all 3 formal systems (Haskell, System F and C) seem to have different design trade-offs.

So what are the consequences of choosing one over the other?

Answer 1

Haskell

This is a strange problem because you are working with the vague concept = . _|_ = _|_ only "contains" (and even then you really should use ⊑ ) at the semantic level of the domain. If we distinguish between information available at the semantic level of the domain and equality in the language itself, then it is perfectly correct to say that True ⊑ x + y == x → True ⊑ y == 0 .

This is not a problem, and these are not natural numbers, which are also a problem - the problem is simply distinguishing between equality in a language and statements about equality or information in the semantics of a language. The lack of a question about the lower parts, we can usually argue that Haskell uses naive equatorial logic. With reason, we can still use equational reasoning - we just need to be more complex with our equations.

A more complete and clear account of the relationship between full languages ​​and partial languages, determined by their uplift, is given in the excellent article " " Quick and free reasoning is morally correct. "

WITH

You claim that C requires that everything (including the address space) have a finite size, and therefore the semantics of C "impose a limit" on the size of representable natural numbers. Not really. The C99 standard states the following: “Any type of pointer can be converted to an integer type. If not specified earlier, the result is determined by the implementation. If the result cannot be represented in an integer type, the behavior is undefined. The result should not be in the range of any integer type. " The rationale document further emphasizes that “C is now implemented on a wide range of architectures. Although some of these architectures have uniform pointers whose size does not exceed an integer type, the most portable code cannot accept any necessary correspondence between different types of pointers and integer types. In in some implementations, pointers can even be wider than any integer type.

As you can see, there is clearly no assumption that pointers should be of finite size.

Answer 2

You have a set of theories as frameworks with which you will reason; ultimate reality, Haskell semantics, System F - only those of them.

You can choose a suitable theory for your work, build a new theory from scratch or from large parts of existing theories put together. For example, you can consider the set of always-ending Haskell programs and use bottomless semantics safely. In this case, your addition will be correct.

For low-level languages, there may be considerations to include finiteness, but for a high-level language, such things should be omitted because more abstract theories allow wider application.

During programming, you do not use the theory of "language specification", but the theory of "language specification + implementation restrictions", so there is no difference between cases where memory restrictions are present in the language specification or in the language implementation. The absence of restrictions becomes important when you begin to build pure theoretical constructions within the framework of linguistic semantics. For example, you may need to prove some equivalence of programs or language translations and find that every unnecessary detail in the language specification brings great pain in the proof.

Answer 3

I am sure that you heard the aphorism that "in theory there is no difference between theory and practice, but in practice there is."

In this case, there are differences in theory, but all these systems deal with the same finite amount of address memory, so in practice there is no difference.

EDIT:

Assuming that you can represent a natural number in any of these systems, you can imagine a complement in any of them. If the constraints you are worried about do not allow the representation of a natural number, you cannot imagine the complement Nat * Nat.

Think of a natural number as a pair (heuristic lower bound on the maximum bit size and lazily evaluated bit list).

In lambda calculus, you can think of a list as a function that returns a function that is called with true, returns 1 bit, and a called with false returns a function that does the same for 2 bits, etc.

Addition is the operation applied to the zip of these two lazy lists that propagate the carry bit.

Of course, you must represent the maximum bit size heuristic as a natural number, but if you only create numbers with the number of bits that are strictly less than the number you represent, and your operators do not violate this heuristic, then the bit size is inductively smaller than the number that you want to manipulate, so the operations are completed.

Regarding the convenience of accounting for edge cases, C will give you very little help. You can return special values ​​to represent overflow / underflow and even try to make them infectious (like IEEE-754 NaN), but you won’t receive complaints at compile time if you can’t check. You can try and overload the SIGFPE signal or something similar to a trap problem.

I can not say that y is zero - if x is the bottom, x + y = x for any y.

If you want to do symbolic manipulation, Matlab and Mathematica are implemented in C and C. However, python has a well-optimized bigint implementation that is used for all integer types. This is probably not suitable for representing really really big numbers.