Newest at the top
| 2024-05-13 21:03:01 +0200 | <tomsmeding> | monochrom: who claims that value? |
| 2024-05-13 21:02:39 +0200 | <monochrom> | But I disdain the "value" in corresponding to verbal reasoning. Natural languages were not intelligently designed. |
| 2024-05-13 21:02:30 +0200 | <mauke> | so far there are three possible universes |
| 2024-05-13 21:01:58 +0200 | <APic> | Yes. |
| 2024-05-13 21:01:47 +0200 | <mauke> | yes |
| 2024-05-13 21:01:42 +0200 | <monochrom> | I acknowledge and like the value of natural deduction in being in perfect correspondence with functional programming. |
| 2024-05-13 21:01:36 +0200 | <tomsmeding> | mauke: it's given that one of the two caskets contains a portrait |
| 2024-05-13 21:01:04 +0200 | <tomsmeding> | where Wiltink interpreted "formalisation" to mean "writing proofs in a formalism", whereas Gentzen perhaps intended it to mean "expressing proofs in terms of axioms" |
| 2024-05-13 21:00:46 +0200 | <mauke> | the solution is clearly that not enough information is given to determine an answer |
| 2024-05-13 21:00:31 +0200 | <tomsmeding> | possibly a confusion of terminology occurred here |
| 2024-05-13 21:00:27 +0200 | <mauke> | I don't understand the problem |
| 2024-05-13 21:00:11 +0200 | <tomsmeding> | the author even quotes Gentzen referring to formalisation of mathematical proofs |
| 2024-05-13 20:59:41 +0200 | <tomsmeding> | being obviously based on the axioms and thus obviously correct is the point, I thought |
| 2024-05-13 20:59:27 +0200 | <tomsmeding> | monochrom: the case of the paper is a bit weird though, I think; the author argues that natural deduction is not great because it is inefficient, but efficiency is not really the point of natural deduction, is it? |
| 2024-05-13 20:58:10 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-13 20:56:24 +0200 | <tomsmeding> | "associativity of ===" is also a funny statement to make to a constructivist |
| 2024-05-13 20:55:57 +0200 | <tomsmeding> | "what does that even mean" |
| 2024-05-13 20:55:43 +0200 | <tomsmeding> | I'm not saying the proof is wrong, but the first step took me embarrassingly long to understand |
| 2024-05-13 20:55:24 +0200 | <tomsmeding> | it is |
| 2024-05-13 20:55:20 +0200 | <monochrom> | It is a correct conflation in classical logic. |
| 2024-05-13 20:54:58 +0200 | <tomsmeding> | feels very weird to read that |
| 2024-05-13 20:54:54 +0200 | <tomsmeding> | that proof on the first page conflates booleans and truth values |
| 2024-05-13 20:53:26 +0200 | gawen | (~gawen@user/gawen) |
| 2024-05-13 20:51:40 +0200 | <tomsmeding> | (hey, a dutchman) |
| 2024-05-13 20:51:17 +0200 | <monochrom> | https://www.cs.utoronto.ca/~trebla/eq-wiltink.pdf shows how to use how xnor aka (==) as a monoid operator to solve a famous logic puzzle. |
| 2024-05-13 20:51:13 +0200 | <zzz> | mauke: thath's fun |
| 2024-05-13 20:48:30 +0200 | <lambdabot> | Foldable t => t Bool -> Bool |
| 2024-05-13 20:48:29 +0200 | <mauke> | :t foldl' (/=) False |
| 2024-05-13 20:48:29 +0200 | zzz | (~yin@user/zero) |
| 2024-05-13 20:47:43 +0200 | <lambdabot> | Bits a => a -> a -> a |
| 2024-05-13 20:47:42 +0200 | <mauke> | :t xor |
| 2024-05-13 20:47:31 +0200 | <tomsmeding> | s/xor/nonempty/ |
| 2024-05-13 20:47:15 +0200 | <glguy> | probably xor had it before getting pulled into base |
| 2024-05-13 20:46:53 +0200 | zzz | (~yin@user/zero) (Ping timeout: 272 seconds) |
| 2024-05-13 20:46:29 +0200 | gawen | (~gawen@user/gawen) (Quit: cya) |
| 2024-05-13 20:44:13 +0200 | <ncf> | why the hell do we have xor :: NonEmpty Bool -> Bool but not [Bool] -> Bool |
| 2024-05-13 20:43:22 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-13 20:37:55 +0200 | <tomsmeding> | zzz: tip: cabal-plan dot --hide-builtin |
| 2024-05-13 20:37:45 +0200 | <zzz> | tomsmeding: ty |
| 2024-05-13 20:37:29 +0200 | <tomsmeding> | cabal-plan dot |
| 2024-05-13 20:36:01 +0200 | <zzz> | how can i visualize a dependency graph? cabal-plan? |
| 2024-05-13 20:34:53 +0200 | <cheater> | like 2-3 screens of code |
| 2024-05-13 20:34:43 +0200 | <cheater> | the examples i'm thinking of are a little more involved than that |
| 2024-05-13 20:26:40 +0200 | roboguy_ | (~roboguy_@216.147.124.110) (Client Quit) |
| 2024-05-13 20:26:34 +0200 | roboguy_ | (~roboguy_@216.147.124.110) |
| 2024-05-13 20:26:28 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-05-13 20:25:34 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds) |
| 2024-05-13 20:22:12 +0200 | <glguy> | at least for the cases that are simple enough for doctest to load them |
| 2024-05-13 20:21:58 +0200 | <glguy> | I do support [Leary]'s suggestion of putting the examples in module comments and using doctest to check them, especially for very limited scope examples: here's how to use just this one function/module |
| 2024-05-13 20:21:13 +0200 | <cheater> | sometimes my own forgetfulness makes me think our memories are just biological cassette tape |