3 ms·

> all mathematical proofs are algorithms They're not. Only constructive proofs have corresponding programs (namely, the program that actually carries out the r

> all mathematical proofs are algorithms They're not. Only constructive proofs have corresponding programs (namely, the program that actually carries out the relevant construction). You can embed nonconstructive proofs indirectly via double-negation translation (computational counterpart: continuation-passing style), but equivalence of classical formulas isn't preserved. > all types are algorithms Definitely not the case. Types correspond to propositions, not their proofs.

peter_d_sherman 4y ago
Let me rephrase then... >all mathematical proofs are algorithms All mathematical proofs consist of a series of steps. >all types are algorithms All types can be expressed as a series of steps -- with a given input -- and an output of True or False following those steps. True if the given input is a member of that Type. False if a given input is not a member of that Type. If the definition of an 'Algorithm' -- is 'a series of steps', then both mathematical proofs and types -- must be Algorithms... If we have any debate -- then we are debating the semantics of "what constitutes a step" -- what rigorously defines it -- and what steps may be permitted when... It may very well be that the Lambda Calculus is the best definition of what constitutes these steps -- but it may very well be that there is a different/better paradigm for looking at them (I don't know myself -- I am trying to determine this)... Here, you might like the following video (graciously submitted by rbonvall!) for an overview of some of the different possible paradigms that these steps -- might be considered in: https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU
- consilient 4y ago
  > All types can be expressed as a series of steps -- with a given input -- and an output of True or False following those steps. No, this is a fundamental misunderstanding of what types are. They're not, in general, subsets of some larger universe of values, and you can't have terms without types attached. (Of course there are "gradually typed" programming languages, but these are really languages with a top type a la `object`, subtyping, and generally a healthy dose of unsoundness).
  - peter_d_sherman 4y ago
    >They're not, in general, subsets of some larger universe of values You have a Computer. The Computer has N bytes of memory. You want to declare a Boolean type variable. You tell your compiler this by coding it in the language of your choice. The compiler will typically allocate 1 to 8 bytes of memory to store that Boolean value -- depending on such things as how many bits your CPU is, what compiler options are, if variables should be byte or dword or qword aligned in memory, etc. >They're not, in general, subsets of some larger universe of values But the thing is, that memory allocated for the Boolean variable is now constrained -- to be a subset of all of the previously permissible bit patterns for that memory. It is constrained to be either 0 (representing False) or 1, (representing True). If that Boolean value is 8 bits long (let's say) -- then the only two permissible possibilties that exist for it -- are either 00000000 (0 - False) or 00000001 (1 - True). >They're not, in general, subsets of some larger universe of values That type, the Boolean -- is very much a subset -- of a larger universe of values... For a given Byte it can also be determined if it belongs to the Boolean Type -- via a simple function (aka "series of steps", aka algorithm). Basically, just compare that Byte's value to 0 or 1. If it's either a 0 or a 1, then it's a member -- and if it isn't one of these values then it isn't. That small series of steps -- is a function. A function which determines membership of given data -- an input (in this case, a byte) -- to a type (in this case, a Boolean type). To validate or repudiate type membership (or lack thereof) of something more complex -- a more complex function/algorithm/series of steps -- may be needed -- but the point is, that's how it's done... >They're not, in general, subsets of some larger universe of values So they are all-inclusive sets of some larger universe of values? ? If that's the case -- then why do neither computer programs nor mathematical constructs that use types -- use a single solitary type that represents the larger universe of all possible values everywhere that a type is used? ?
    - consilient 4y ago
      > The Computer has N bytes of memory. You want to declare a Boolean type variable. You tell your compiler this by coding it in the language of your choice. The compiler will typically allocate 1 to 8 bytes of memory to store that Boolean value -- depending on such things as how many bits your CPU is, what compiler options are, if variables should be byte or dword or qword aligned in memory, etc. You're confusing several things here. - a term is not its runtime representation - a type is not the set of all terms that inhabit it (though you can get away with pretending it is in simple cases) - and more generally, operational semantics are not denotational semantics > So they are all-inclusive sets of some larger universe of values? No, they're simply not sets. Types are primitive notions in type theories, the same way that sets are the primitive notions of set theory. No reduction of one to the other is necessary or, typically, desirable. And even if you try to build type theory on set-theoretic foundations - which is 100% the wrong choice if you want to apply it to computational problems down the line - you're still going to run into problems once things start getting recursive. Consider, for example, the type of "hyperfunctions" given by `type Hyper a b = Hyper b a -> b` This is too big to be a set, for the usual self-containment reasons. But it's a perfectly legitimate Haskell type, modulo syntax. I've used it in real code. > use a single solitary type that represents the larger universe of all possible values everywhere that a type is used? That's what a dynamically typed programming language is.

peter_d_sherman 4y ago

Let me rephrase then... >all mathematical proofs are algorithms All mathematical proofs consist of a series of steps. >all types are algorithms All types can be expressed as a series of steps -- with a given input -- and an output of True or False following those steps. True if the given input is a member of that Type. False if a given input is not a member of that Type. If the definition of an 'Algorithm' -- is 'a series of steps', then both mathematical proofs and types -- must be Algorithms... If we have any debate -- then we are debating the semantics of "what constitutes a step" -- what rigorously defines it -- and what steps may be permitted when... It may very well be that the Lambda Calculus is the best definition of what constitutes these steps -- but it may very well be that there is a different/better paradigm for looking at them (I don't know myself -- I am trying to determine this)... Here, you might like the following video (graciously submitted by rbonvall!) for an overview of some of the different possible paradigms that these steps -- might be considered in: https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU

consilient 4y ago
> All types can be expressed as a series of steps -- with a given input -- and an output of True or False following those steps. No, this is a fundamental misunderstanding of what types are. They're not, in general, subsets of some larger universe of values, and you can't have terms without types attached. (Of course there are "gradually typed" programming languages, but these are really languages with a top type a la `object`, subtyping, and generally a healthy dose of unsoundness).
- peter_d_sherman 4y ago
  >They're not, in general, subsets of some larger universe of values You have a Computer. The Computer has N bytes of memory. You want to declare a Boolean type variable. You tell your compiler this by coding it in the language of your choice. The compiler will typically allocate 1 to 8 bytes of memory to store that Boolean value -- depending on such things as how many bits your CPU is, what compiler options are, if variables should be byte or dword or qword aligned in memory, etc. >They're not, in general, subsets of some larger universe of values But the thing is, that memory allocated for the Boolean variable is now constrained -- to be a subset of all of the previously permissible bit patterns for that memory. It is constrained to be either 0 (representing False) or 1, (representing True). If that Boolean value is 8 bits long (let's say) -- then the only two permissible possibilties that exist for it -- are either 00000000 (0 - False) or 00000001 (1 - True). >They're not, in general, subsets of some larger universe of values That type, the Boolean -- is very much a subset -- of a larger universe of values... For a given Byte it can also be determined if it belongs to the Boolean Type -- via a simple function (aka "series of steps", aka algorithm). Basically, just compare that Byte's value to 0 or 1. If it's either a 0 or a 1, then it's a member -- and if it isn't one of these values then it isn't. That small series of steps -- is a function. A function which determines membership of given data -- an input (in this case, a byte) -- to a type (in this case, a Boolean type). To validate or repudiate type membership (or lack thereof) of something more complex -- a more complex function/algorithm/series of steps -- may be needed -- but the point is, that's how it's done... >They're not, in general, subsets of some larger universe of values So they are all-inclusive sets of some larger universe of values? ? If that's the case -- then why do neither computer programs nor mathematical constructs that use types -- use a single solitary type that represents the larger universe of all possible values everywhere that a type is used? ?
  - consilient 4y ago
    > The Computer has N bytes of memory. You want to declare a Boolean type variable. You tell your compiler this by coding it in the language of your choice. The compiler will typically allocate 1 to 8 bytes of memory to store that Boolean value -- depending on such things as how many bits your CPU is, what compiler options are, if variables should be byte or dword or qword aligned in memory, etc. You're confusing several things here. - a term is not its runtime representation - a type is not the set of all terms that inhabit it (though you can get away with pretending it is in simple cases) - and more generally, operational semantics are not denotational semantics > So they are all-inclusive sets of some larger universe of values? No, they're simply not sets. Types are primitive notions in type theories, the same way that sets are the primitive notions of set theory. No reduction of one to the other is necessary or, typically, desirable. And even if you try to build type theory on set-theoretic foundations - which is 100% the wrong choice if you want to apply it to computational problems down the line - you're still going to run into problems once things start getting recursive. Consider, for example, the type of "hyperfunctions" given by `type Hyper a b = Hyper b a -> b` This is too big to be a set, for the usual self-containment reasons. But it's a perfectly legitimate Haskell type, modulo syntax. I've used it in real code. > use a single solitary type that represents the larger universe of all possible values everywhere that a type is used? That's what a dynamically typed programming language is.