@mudri@mathstodon.xyz avatar

mudri

@mudri@mathstodon.xyz

(2022-11-10) Programming Languages at Huawei. Sticking around for a PhD with https://types.pl/@bentnib at Strathclyde, mechanising linearity.

This profile is from a federated server and may be incomplete. Browse more on the original instance.

boarders, (edited ) to random
@boarders@mathstodon.xyz avatar

Andrej Bauer gave an excellent recent talk “How to not believe in the law of excluded middle”: https://youtu.be/96iHUx0aGDs?si=y9j8Kc9znPs-cS1U

Towards the beginning he mentions some bad reasons for not believing in excluded middle include the undecidability of CH. This is true, but I don’t think it is a bad thing to mention (or perhaps I just feel bad since I am guilty of having done so) since:

  • CH ∨ ¬CH - “CH is either true or false” is a theorem of ZFC since it is just an instance of LEM. This is obviously not a solution to Hilbert’s first problem

  • Pr(CH) ∨ Pr(¬CH)- “there is a proof of CH or a proof of its negation in ZFC”. This is is not true, as shown by Cohen + Gödel (this is not an internal statement in ZFC, it is meta-theoretical)

  • Dec(Pr(CH)) - it is decidable that we can give a proof of CH, or that we can’t give a proof. This is also true, but this time we can’t appeal to LEM so we must be appealing to something else (in this case we appeal again to Cohen + Gödel). But this means we don’t accept the meta-theoretic principle LEM when it comes to statements about provability

mudri,
@mudri@mathstodon.xyz avatar

@boarders Come to think of it, how do you define Dec when your (meta)theory has excluded middle and global choice? When you have a parameter to a predicate, you can talk about Turing machines that input that parameter and output a result, but for unparametrised propositions, you can “decide” them in the metatheory and just have a Turing machine that is constantly 0 or 1, as appropriate.

chrisamaphone, to random
@chrisamaphone@hci.social avatar

i just got into a groove defining a bunch of relations in agda and straight up just forgot i wasn't using a logic programming language (and, therefore, could define a functional relation as... a function)

mudri,
@mudri@mathstodon.xyz avatar

@chrisamaphone Maybe the functional relation is still good to have, though.

christianp, to random
@christianp@mathstodon.xyz avatar

Would any people be able to talk to me about the similarities between "simplification" of mathematical expressions, and type-theoretic proofs?
Like, a common task in computer algebra is to automatically rewrite expressions to a "simpler" form. Ideally, you'd have a proof that the simplified expression is equivalent to the original. Could this sort of thing fall out of Lean naturally?

mudri,
@mudri@mathstodon.xyz avatar

@christianp This sort of thing can't really be said to “fall out naturally” in most cases. For a given algebraic theory (e.g, rings), you typically have to define the types of expressions (e.g, terms made of 0, 1, +, ×, and variables)) and normalised expressions (e.g, polynomials with coefficients from ℤ) manually inside the proof assistant, together with the manually written normaliser and stuff to connect the types of expressions with the subset of type theory expressions you're actually interested in. These manually written things are just like ordinary functional programming.

The few cases that do fall out somewhat naturally are where the type theory already contains a type usable as the type of normalised expressions. The most obvious case is where you're interested in the type theory itself, or some fragment of it, which the implementation will happily normalise terms of automatically. The other notable cases in most implemented type theories are monoids and categories, which fall out from functions having a unital and associative composition up to definitional equality, meaning that the type theory already “knows” how to decide equality in those theories.

dpiponi, to random
@dpiponi@mathstodon.xyz avatar

Too much of my life spent wrangling build systems rather than writing actual software that does something.

mudri,
@mudri@mathstodon.xyz avatar

@christianp @dpiponi @SvenGeier I'd have gone for the tune of Girls & Boys.

mudri,
@mudri@mathstodon.xyz avatar

@christianp @dpiponi @SvenGeier Girls who are boys who like boys to be girls /
Who do boys like they're girls, who do girls like they're boys /
Always hand in hand though their parklife

jonmsterling, to random
@jonmsterling@mathstodon.xyz avatar

How true this is, and the inelegant phrasing does not make it less true! We are guilty as charged... https://borretti.me/article/type-inference-was-a-mistake

mudri,
@mudri@mathstodon.xyz avatar

@d_christiansen @jonmsterling I think the idea of having “no type inference” in C-like syntaxes relies on, at least, not treating projectends (terminology? I mean struct-like expressions whose members are being assessed) as expressions. You also have to make sure functions being applied are not expressions, but this may be, or historically may have been, true of many such languages. People using C-like syntaxes tend to conflate “type inference” with type inference for local variable declarations, of which the greatest benefit is eliminating the Java-ism Foo foo = new Foo(). But this conflation only makes sense by ignoring the things I mentioned at the start.

christianp, to random
@christianp@mathstodon.xyz avatar

Having to bite my fist: mustn't upset people who don't know better.

My colleague in the central EDI team publishes a newsletter. He's not at all technically minded, so he uses Microsoft Sway, since it's there and it seems to look nice.

It reloads the page when you resize the window! It forces you to reload the page if it's been open for "too long"!
WHAT

The newsletter contains some audio files (which he thinks are podcasts) and videos, which can't be opened in a new tab or linked to. They can't even be downloaded: I tried to get their URL from the inspector, and they're only fetched as fragments by repeated requests, instead of just downloading the file.

ARGRGRRRGRGRGR

mudri,
@mudri@mathstodon.xyz avatar

@christianp It ruins the test a little that the link appears right in the middle of the focus. But indeed, it's quite hard to see at normal size.

johncarlosbaez, (edited ) to random
@johncarlosbaez@mathstodon.xyz avatar

I decided to see how my research has changed over time by making word clouds based on Google Scholar.

Here's what I wrote about from 1985 to 1995. At this early stage of my career I was doing traditional mathematical physics. I got tenure based on my work on quantum and classical field theory - for example, scattering and complete integrability for classical field theories like Yang-Mills theory.

After I got tenure, I got excited about how knot theory is connected to quantum gravity.

Later things changed....

(1/n)

mudri,
@mudri@mathstodon.xyz avatar

@johncarlosbaez “Octonions and Superstring Theory” in Japanese

mudri, to random
@mudri@mathstodon.xyz avatar

Maybe having a bad idea of my audience's preconceptions is better than having no idea, so here goes...

If I say “environment” in a programming language context, what sort of thing(s) do you think of? What uses do you know of “environments”? I think there are lots of right answers; please, collectively, tell me all of them!

Boosts welcome.

mudri,
@mudri@mathstodon.xyz avatar

@christianp @pozorvlak My main use doesn't appear in this list, by the way. 😉

christianp, (edited ) to random
@christianp@mathstodon.xyz avatar

The following will probably only make sense to people in the UK.

I have a vague sense that the job of "lollipop person" used to be fairly strongly gendered, but I can't remember which way - is it lollipop man, or lollipop lady? I feel like "lollipop lady" sounds more like what I said growing up, but both lollipop people at my kids' school are men and I've overthought it and now I'm suffering from semantic satiation.

So, was it a lollipop man or a lollipop lady when you were at school?

mudri,
@mudri@mathstodon.xyz avatar

@christianp @mark It would invariably be “dinner lady” where I grew up, which I guess motivates more of this weird artificial “midday supervisor” phrasing.

mudri,
@mudri@mathstodon.xyz avatar

@christianp @mark It misses a chance for alliteration, but there's something to be said for its trochaic metre.

mudri, to random
@mudri@mathstodon.xyz avatar

Are I right in thinking that if you have a fine-grained language (like FGCbV) and you want to give it an operational semantics with environments (like a CEK-machine), you should include closures in the language's syntax? Otherwise, I suppose you have to have a pass that traverses every value coming from the program to put environments into the right places before they hit the rest of the machine, or something like that.

mudri,
@mudri@mathstodon.xyz avatar

@jonmsterling Ah, good point. Indeed, it's the control string (C) that needs closures, and that can be thought of as separate from the language.

boarders, to random
@boarders@mathstodon.xyz avatar

What are some compelling ways to explain type theory to someone without a mathematics background, are there some particular interesting results one could showcase?

mudri,
@mudri@mathstodon.xyz avatar

@boarders I guess canonicity is quite a cool and unique result (when it holds). It gives you confidence that, whatever fancy higher order stuff you use, first order results are going to be the concrete things you expect them to be.

christianp, to random
@christianp@mathstodon.xyz avatar

NCL 🚆 EDI

If you're a seal on the north sea coast, I will wave at you.

mudri,
@mudri@mathstodon.xyz avatar

@christianp I'll be following later in the day!

mudri, to random
@mudri@mathstodon.xyz avatar

My hot take, if it turns out that Othello has indeed been weakly solved as a draw, is that the game really is flawless, in a sense. Simple and tractable rules, no time attacks, and, we now know, balance between the two players despite the initial and final asymmetry.

Flaws in other abstract games I'm familiar with:

  • Chess piece movements are obviously pretty arbitrary – hence the family of related traditional games. There is also bullshit like castling and en passant, which suggests that the game without them is flawed (I'm not exactly sure how).
  • Chess and go both have super-kou rules (“threefold repetition” in chess) which, in general, require players to remember and recognise significant amounts of game history to enforce correctly. They are flawed without such rules (and even one of the two plausible go super-kou rules is flawed). Othello, quite obviously, can't have repeated states.
  • Go with area scoring allows players at the end of the game to play lots of moves without penalty – sometimes forcing a response from the opponent and running their clock down. With territory scoring, they can do the same but with punishment (not that punishment means much if they know that they're losing). But territory scoring is also flawed – hypothetical play, ending book, &c. Othello ends after at most 60 moves.
  • Chess tends towards draws in high-level play, but a draw is a boring result in chess (like in cricket). Go almost certainly favours the first player, so in modern times, people invariably give the second player a few points' head start to fix that. In Othello, a draw is an exciting result – both players nearly won (like a tie in cricket).

(I should say: They're all still great games.)

mudri,
@mudri@mathstodon.xyz avatar

@boarders Maybe I should have stuck to the football analogy of a 0-0 draw vs a 3-3 draw. 😂

etherdiver, to random
@etherdiver@ravenation.club avatar

If you can see this post and you are under 30 years of age I want you to suggest a band for me to check out. Something of "your generation" tho; I know the old-man shit very well, thanks.

Electronic based acts preferred cause that's what I like but I am capable of appreciating anything, so if it's That Fucking Good, bring it!

mudri,
@mudri@mathstodon.xyz avatar

@etherdiver Probably the closest I get to electronic is Arcane Roots (recommend: Melancholia Hymns), and Future of the Left switch out guitar for synth on a few tracks (recommend: The Plot Against Common Sense, probably, but they're fairly consistent).

mudri, to random
@mudri@mathstodon.xyz avatar

It's been a while coming, but I formally submitted my PhD thesis earlier today.

A Framework for Semiring-Annotated Type Systems
https://personal.cis.strath.ac.uk/james.wood.100/pub/thesis.pdf

Abstract:
The use of proof assistants as a tool for programming language theorists is becoming ever more practical and widespread. There is a range of satisfactory implementations of simply typed calculi in proof assistants based on dependent type theory.

In this thesis, I extend an account of Simply Typed λ-calculus so as to be able to represent and reason about calculi whose variables have restricted usage patterns. Examples of such calculi include a logic with an S4 □-modality, in which certain variables cannot be used “inside” a box (□); and Linear Logic, in which linear variables have to be used exactly once. While there are existing implementations of some of these calculi in proof assistants, many of these implementations share little with the best presentations of simply typed calculi without variable usage restrictions, and thus end up being poorly understood or suboptimal in facilitating mechanised reasoning.

Concretely, the main result of this thesis is a framework for representing and reasoning about a wide range of calculi with restricted variable usage. All of these calculi support novel simultaneous renaming and substitution operations. Furthermore, I provide several other examples of generic and specific programs facilitated by the framework. All of this work is implemented in the proof assistant Agda.

mudri,
@mudri@mathstodon.xyz avatar

@BoydStephenSmithJr Good question. All of the object languages I consider are non-dependently typed, and even non-polymorphic (though System F-like polymorphic systems may be in reach), which rules out GRTT. However, simply typed versions of GRTT and QTT are both in scope. (They end up being very similar, but with different ⊗-elimination rules IIRC. I mention the GRTT-style ⊗-elimination rule in section 4.4.1.)

In any case, I would say something like “treat” or “support” instead of “build on” or “replace”, given that the main contribution is abstracted one level away from any particular syntax, and the supported systems become instances of the more general definition.

Private
mudri,
@mudri@mathstodon.xyz avatar

@RanaldClouston @rugby Just like APL programmers.

christianp, to random
@christianp@mathstodon.xyz avatar

Dreamt I was stuck in London and needed to eat. My friend took me into a goth-themed chain restaurant. Everything on the menu was pretentious and eldritch and I hated it so much I woke up

mudri,
@mudri@mathstodon.xyz avatar

@christianp Is this what goths are into these days? I still think of the emo-like ones of the '00s.

julesh, to random
@julesh@mathstodon.xyz avatar

Idle thonk: the fundamental theorem of arithmetic, in the form "the free commutative monoid on the free monoid on a point is multiplicative positive integers" is, like, the simplest not-boring consequence of the periodic table of monoidal n-categories

mudri,
@mudri@mathstodon.xyz avatar

@julesh Specifically, the construction here is via (\mathrm{Set} \overset{F}\to \mathrm{Mon} \overset{U}\to \mathrm{Set} \overset{F}\to \mathrm{CMon}), I suppose.

johncarlosbaez, (edited ) to random
@johncarlosbaez@mathstodon.xyz avatar

NOTE: I quoted a report from an executive of DuckDuckGo attending the antitrust lawsuit against Google. This article has now been retracted from Wired:

"After careful review of the op-ed, "How Google Alters Search Queries to Get at Your Wallet," and relevant material provided to us following its publication, WIRED editorial leadership has determined that the story does not meet our editorial standards. It has been removed."

I hope we'll learn more about what Google actually does, since September 28, the court established a process allowing the Justice Department to publish more information about this case.

https://www.wired.com/story/google-antitrust-lawsuit-search-results/

mudri,
@mudri@mathstodon.xyz avatar

@johncarlosbaez @MartinEscardo I've used DuckDuckGo for a while now, but I don't entirely trust it to stay good. I've seen adverts around for DuckDuckGo Browser, which strikes me as a land-grab rather than a worthwhile project (given that Firefox is already a perfectly acceptable browser, once you change the default search engine). It also promotes this weird conflation of browser and search engine that a lot of people seem to have picked up recently.

  • All
  • Subscribed
  • Moderated
  • Favorites
  • JUstTest
  • ethstaker
  • thenastyranch
  • ngwrru68w68
  • magazineikmin
  • khanakhh
  • rosin
  • mdbf
  • Youngstown
  • slotface
  • everett
  • cubers
  • kavyap
  • DreamBathrooms
  • provamag3
  • InstantRegret
  • Durango
  • normalnudes
  • osvaldo12
  • tacticalgear
  • cisconetworking
  • Leos
  • GTA5RPClips
  • modclub
  • anitta
  • tester
  • megavids
  • lostlight
  • All magazines