gylterud

10 ms·

91.
by gylterud 3y ago
I usually joke, when someone has their bike stolen, that they have just gained membership in the local, involuntary bikesharing community, and thus can help themselves to a another bike from the bike parking.
92.
by gylterud 3y ago
Agda is a nice language with a good homotopy type theory library based on the univalence axiom called agda-unimath.
93.
by gylterud 3y ago
Type theories usually come with a reduction relation on terms. It computes things like β-reduction for function, inserting arguments into function bodies, computes projections out of tuples, etc A normal term is one where no further reducti
94.
by gylterud 3y ago
Interestingly, even thought type-in-type is inconsistent, there are no normal terms of the “empty” type. So, if you restrict to normal terms you do not get full explosion. There are however types A such that both A and not A have normal ter
95.
by gylterud 3y ago
> various versions of Martin-Löf’s intuitionistic type theory and finally the calculus of constructions of Coquand and Huet. In every case, they were created with no interpretation in mind. They were justified syntactically, for example
96.
by gylterud 3y ago
«A neighborhood of infinity» was one of the blogs which inspired me as a young person, and definitely put me on the path to do research. I would spend hours reading the posts, testing the code and trying to use the stuff in my own programs.
97.
by gylterud 3y ago
Came here to mention this exactly. I have a quick intro to the compose key on my website [0] and an intro for how to use Unicode with Latex[1], and there are other resources around the web if you are looking. The idea of a compose key for U
98.
by gylterud 3y ago
We (in Norway) also recognise that it is not really discrete. In school we learned about the different dialectical traits (like palatalisation, different versions of “r” as well as morphological and lexical differences) and the different ar
99.
by gylterud 3y ago
How about an automatic nationalisation in stead? Where you take companies which have grown too big out of the private ownership’s hands.
100.
by gylterud 3y ago
It depends on believing in classical logic. Constructive mathematicians can instead choose to adopt intuitionistic logic and postulate Church thesis, which states that all functions, and thus sequences, are computable.
101.
by gylterud 3y ago
There is Kolmogorov complexity, which is (relative to a programming language) a measure of how easy a sequence is to produce algorithmically – i.e. what is the length of the shortest program which can produce the sequence. Most mathematicia
102.
by gylterud 3y ago
The AB patterns in the article remind me a bit of the sequences which occur in “The anti-pattern game” – a game I invented for a course I took in modal logic. The game produces sequences where no pattern repeats more than twice in a row: ●
103.
by gylterud 4y ago
There is the theory of containers (unrelated to the docker kind). They represent functors on sets and the differential operator on them satisfies the usual laws. In short a container is a set of shapes and a set of positions for data in eac
104.
by gylterud 4y ago
Fortran will get generics soon(ish).
105.
by gylterud 4y ago
Cool! I tried to play DnD with it. At first it refused, but a bit of preparation questions, me prefixing with Player 1: and telling it to respond with DM: My wizard Grok got to go to the Tomb of The Orb of Infinite Power and do some cinema
106.
by gylterud 4y ago
Indeed – the first thing I did in Midjourney was to create this for my upcomming D&D campaign, set in a dessert world: https://hakon.gylterud.net/img/dessert_mindflayer-scaled.jpg
107.
by gylterud 4y ago
> kjølen can mean "the fridge" as in "put something in the fridge"/"put something in a cool place" I could be wrong, but I would guess "kjølen" would translate to the "the keel" in t
108.
by gylterud 5y ago
I wrote a simple script[0] which generates a new address for each site I register. Then a simple script to look up what the generated address was later. It is written for OpenBSD, but should be easy to adapt. [0]: https://hakon.g
109.
by gylterud 5y ago
This might be what I need. A few years ago I made a short tutorial on YouTube self-defence [0] but the measures are quite drastic. [0]. https://hakon.gylterud.net/tutorials/youtube.html
110.
by gylterud 6y ago
I like when YouTubers talk about other channels they like, and I often go check those out – especially if they are on some completely different topic. Because if someone is making content I like, they might also have good taste when it come
111.
by gylterud 6y ago
I found YouTube suggestions to be generally useless, so I have just disabled the suggestion sidebar completely[0]. Leaves more screen space for the video. The reason I found them useless is that the suggestions were too specialised. I usual
112.
by gylterud 7y ago
> Thirdly, the cost is not large. Businesses are already absorbing the lost productivity caused by the fathers being exhausted. This formalizes it. Exactly! And in both Norway and Sweden you can be part time on leave. For some time I ha
113.
by gylterud 7y ago
When we had our first child (in Sweden), we could divide the time (13 months total) freely between the two of us. Then we got some extra money if each of us took more than 30% of that time. I think they stopped with the money bonus, but it
114.
by gylterud 7y ago
Are you talking about running ssh-agent on the server side? To further connect to some other machine? For that I use a file to save the name of the socket and PID, and restore this in my .profile.
115.
by gylterud 7y ago
However, even with positive expectation value, you should not always play. One should first check the Kelly criterion, which is well explained Russel O’Connor’s blog post: “Do Not Play the Lottery Unless You Are a Millionaire” http:/&
116.
by gylterud 7y ago
Agda[0] and Coq and other languages for formalising mathematics (they are also programming languages) make a lot of use of Unicode to make the mathematical statements readable. Here is an example: > ∑-+-distribute : ∑ (A + B) C ≃ (∑ A (C
117.
by gylterud 7y ago
Just dropping by to say thank you for running rolz! My role-playing group use the site for dice rolling every week. We have been doing so for more than a year now, and it has been great.
118.
by gylterud 7y ago
EDIT: It is a fair point that it is difficult to say what is easier to implement (the below expands on this). By type theory being natural I was mostly thinking of the fact that it is basically a functional programming language with a very
119.
by gylterud 7y ago
While I agree that one could take caution when studying proposed alternative foundations of mathematics (there are a lot of dysfunctional theories out there, and the link may be one of them for all I know), I think it is unfair to presume i
120.
by gylterud 7y ago
Interpreting A⇔B⇔C as (A⇔B)⇔C is utterly non-standard, but admittedly interesting. A⇔B⇔C is usually not a valid expression in any mathematical formalism. But if used informally, A⇔B⇔C is usually meant to mean (A⇔B)∧(B⇔C), just as when you

More ›