/sci/ - Science & Math

Computer science code monkeys are not welcome to /sci/. >>>/g/tfo

HoTT is a scam invented by CS professors to con money out of grant committees. I've yet to see a serious result from type theory that isn't just a shallow relabeling of things proven in more serious branches of logic.

Nobody likes my book and says they like it with a plainly formatted English language statment
>if like=1
>then fprintf("Nice book Jonathan Tooker")
>else fprintf("le schizo viXra may mays)

The General Relevance of the Modified Cosmological Model
MIRROR 1: http://vixra.org/abs/1712.0598
MIRROR 2: http://2occatl.net/1712.0598v2.pdf
MIRROR 3: https://drive.google.com/file/d/1sXrFZhMo9OjoauL0SgAvpSxD_8qaAYi0/view?usp=sharing

>>9520794
Well, the author list features a couple of well-known mathematicians, including one (more?) Fields Medalists. HoTT is only a couple of years old, and even if I rejected the homotopical part of the book, it would be a very nice introduction to dependent types.
I was much more disappointed by reading about category theory, which was equally hard to understand than type theory, but so much less useful in the end. I guess it’s just not my cup of tea :-/

>>9520794
Vladimir Voevodsky was definitely not CS scum

If yyou don't mind me stealing some of your time:
I'm moving to another country by plane and aside from some clothes and my laptop, I will bring my music instrument.
The case dimensions are 123 x 38 x 21 cm.

The airlines, however, state this:

For health and safety reasons Ryanair does not accept for carriage any individual item exceeding 32 kilos or with combined dimensions of more than 81cms (height), 119cms (width) and 119cms (depth). This weight limit does not apply to mobility equipment.

Now, I think it will fit, but I do not know what they hint towards with 'combined dimensions'.

What are your thoughts? I'm retarded and don't want to risk having to put it on hold.

>>9520823
> 'combined dimensions'.
Sounds very enterprise nonsensy. When I went to the US (from Germany) I flew Iceland or Singapore Air which were quite pleasant, I’ve heard only shitty things about Ryanair so far though so make sure you’ve really got your baggage right.

How about you ship your instrument via umm shipping, would that be an option?

>>9520829
I booked an extra seat for the instrument because it's rather fragile. I would never trust shipping or even 'checked luggage'.

I think I'm fine, anyway. If their 'combined dimensions' was a cube, the instrument would easily fit within it. I'm just paranoid about the max height number, which I exceed with a mere 4 cm.

>>9520850
»Instrument«, I get it ;-)

>>9520853
Plot twist indeed

>>9520853

>>9520870
Interesting! What is it? That old Syrian instrument, what’s it called, Lut?

>>9520875
It's an archlute, a western adaptation of the 17th century. The lute came into Europe somewhere around 700, mostly through the Arabs in Southern Italy and Spain.

>>9520887
Funny, I went to a lute concert last month by accident – I didn’t know what I was getting into and then this guy started taking a seat on stage and played songs about the Euphrates, and told stories about how Flamenco was heavily influenced by Arabian music.

>>9520791
>left physics for computer science

>>9520894
Well, I graduated, and took a job that I quite enjoy. During my studies I used a lot of C++ and Mathematica (was one of the founders of mathematica.stackexchange.com) so I knew a bit about programming, then got hooked on Haskell and from there it was a slippery slope to learning about type theory on the theoretical, and compilers on the practical side. I’ve got a very nice job working on a compiler nowadays, so I’d say it paid off. High energy particle physics jobs are fairly rare on the free market ;-)

>>9520904
whatever you say code monkey

>>9520791
We homotopies now.

I studied the then-version of the book a few years ago, when a release had just came out. What has changed since then? What new developments have I missed?

>>9520791
why should i care about anything homotopy, are there any useful results you could explain to a 12 year old or is this just pure autism as usual

>>9520914
git diff :-P
All I know about HoTT is from the book, I’m not following current research on the topic. It’s just a hobby. But I’ve heard people talk about it on conferences a couple of times, typically with a doubting »I don’t think this is worth it« mindset.

>>9520924
At 12 we learn things like [math](a+b)^2 = a^2+2ab+b^2[/math], I don’t think that’s a good age to measure human achievement by.

>>9520927
thought so

>>9520931
Well, there’s only so much you can do in life, and mathematics is a fairly lonely hobby. I found it very surprising how much of a time vs money trade getting a job was – I thought I spent a lot of time studying/working at uni, but boy is it different compared to a daytime job.

If you’re more knowledgeable, I’ve got a question (normal MLTT): an existentially quantified type can fairly easily be translated to a universally quantified one, [eqn]\sum_{x:A}P(x) = \prod_{y:B}\left(\prod_{x:A} \bigl(x,P(x) \bigr)\rightarrow y)\right) \rightarrow y[/eqn] – is the reverse possible as well somehow? I couldn’t come up with a proof in Agda, but also not a proof of its impossibility :-( (Let’s see how my Latex skills are holding up, fingers crossed…)

>>9520905
Got eeeeeem, epic troll xD

>>9520904
>was one of the founders of mathematica.stackexchange.com
Thank you for your service.

>>9520955
You’re welcome! I learned quite a bit just hanging around there, and even got a free T-Shirt. Hooray! I wear it when bouldering mostly, gotta bring the math to the mountains ;-)

>>9520951
That proposition doesn't make sense to me. Can you explain it? (Is y even a proposition?)

>>9520967
Hacked together on the fly in a tiny textbox. Pic related, a proper version of it, captured from the HoTT intro section.
The general idea is that an existential type can be encoded using only universal quantifiers (as a rank-2 type). My question would now be whether we can somehow use existential quantifiers to encode an existential, going the other way round.
Application: Haskell only has universally quantified types (and rank-N with a language extension), allowing us to express existentials in it. Would it be possible to have a (granted, very esoteric) type system with only existentials that would be just as powerful?

>>9520975
Hah!

>>9520791
Hey man, long time no see.

For better or worse, I never really stopped shitposting on /sci/. During that time when I was around the corner form you in Germany, I also got into HoTT a little bit and last year eventually started doing youtube videos on dependent type theory, although it diverged into a smart contract programming series and now I'm waving back into math. Those things can be combined though, e.g. in
https://youtu.be/T9z3YQkKCLo
And I never stopped following Schreiber at the nLab who does physics in categories that are models for HoTT etc.
https://youtu.be/_O41kh0z_UM
I remember teaching you hom-functors with paint drawings :D Good you know more than me now.
in any case, one may move from one institution and faculty to the other, but I consider the distrinction between physics, math and computer science merely a social seperation of academics, and not a line you could evend draw throught the subject themselves. Best be looking at what all of those have to offer and do your own thing in the middle.

I was thinking about doing a light Curry-Howard shilling clip on the weekend..

>>9521210
Ha wow, nice to hear from you again! Did you stay in academia then?

> I remember teaching you hom-functors with paint drawings :D Good you know more than me now.
Ummm I forgot most of it again ;-)

>>9521216
No I didn't, I work in Augmented Reality now. Pretty cash.

Also, if you're interested I incidentally wanted to start working on a Haskell compiler project that would result in a $60,000 price money. As an expert, you'd do end up doing much more coding than I in the end, but if you're interested agreeing to $30,000 too, I have a job :)

I wrote an interpreter for the STG if that counts. And readlng the GRIN paper has been on my list for a while…
I’m a bit short on time these days though, sports and thinking pretty much switched roles in my life.
What’s that compiler project about?

Nevermind if you're not hungry.

What's STG?

Is this GRIN?
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=E41D44B622B33450A3F06F547B1E61C2?doi=10.1.1.27.3918&rep=rep1&type=pdf

>>9521254
STG is the abstract machine that runs Haskell in GHC, in a nutshell. It’s what has an explicit stack and heap, and proper operational semantics. The readme on Github (»STGi« it’s called) is a bit more precise.

That link looks about right!

Gotta go now, train is arriving, visiting parents etc :-) You’ll find my real email I’m sure. Have a nice evening! (And everyone else as well.)

>>9520791
Newfag here who dis

>>9521463
Sup, I am (was) a tripfag back in the days when /sci/ was founded, around 2010/11/12, when I was finishing my Bachelor’s in (experimental) physics, before doing a master’s in theoretical physics. I talked a lot about math and relativity and the quantum world around here, but then lost interest and didn’t come here until now, when I realized I still had my tripcode lying around. And, to my surprise, googling my name with 4chan actually turned up some results.

Back then this board was quite active (no idea how it’s nowadays), people were sometimes discussing proper science, but other than that it was the usual 4chan shitshow. ICP brought up their »fuckin magnets how do they work« song so /sci/ was flooded with memes, [math]0.999\ldots\neq1[/math] trolls posted hourly, we had lots of infinite forces hitting walls of diamond, and we found out that [math]E=c[/math] thanks to Dr. Werner (»homeopathy with Dr. Werner« on Youtube).

Other tripfags I remember were Physics Guy, at the time doing a PhD I believe at CERN, and Harriet/EK which were desparate for attention without knowing shit about anything science, and being fully aware of that.

Oh, and the Emma Stone guy from above was also around during those days, except it seems he never left. :-)

>>9521614
There's a poster now who does topological quantum field theory and posts Yukari (from Touhou) a lot. Maybe you two can duke it out.

>>9521614
I miss the 0.999 threads.

>>9521614
Still pretty active. Main difference is that instead of meme shitposting we have /pol/ shitposting. Oh and we two have new schizophrenic attention whores.

>>9521731
They still happen quite often, idiot.

>>9521739
No they don't.

>>9521761
>>/sci/?task=search&ghost=yes&search_text=999

>>9521614
big shitposting memes these days are flat earth and racial iq (and iq in general)

>>9521770
lol

Forgot I had these trips, this is fun.

[math]\begin{align*} A = \begin{pmatrix} a & a & a & a & a & a & a & a & a & a & \\ a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\a & a & a & a & a & a & a & a & a & a & \\\end{pmatrix} \end{align*} [/math]

>>9520975
Oh, I see! That makes sense. Apparently I'm rustier than I thought.

>Would it be possible to have a (granted, very esoteric) type system with only existentials that would be just as powerful?
That depends on what other primitive type operators you allow, I think. Are there simply-typed functions? Without them, you have a hard type even expressing a sum type, as a sum type has a parameter of type (A -> Type). What else might you consider as valid primitive types, if not product types?

>>9521909
Hmm, good point. I guess my mistake was that a [math]\Sigma[/math] type is not simply some »[math]\Sigma_{x:A}P x[/math]«, but rather the collection of how to create and annihilate values of that type, and for those we need dependent functions, and for those we need [math]\Pi[/math] types.
In other words, the question was probably wrong, but it took someone else to make me realize it. Thanks :-)

what do you have to say to this???:

https://www.youtube.com/watch?v=kxuU8jYkA1k

>>9523038
When I read the book some years ago I wondered about the minimal formulation of the dependent types formulation and ased a question here

https://cstheory.stackexchange.com/questions/27400/minimal-specification-of-martin-l%c3%b6f-type-theory

(cont.)

oh and I just remembered that at one point I wanted to write down the semantic/category theoretic dependent product definition more clearly than is done on the nLab, so I'm gonna post those two pages and maybe it helps.
I framed it in a very fibre bundle kind of way

start reading at the Discussion section, the abstract definition above can only make sense after

Oh wait, I even have notes on the product for a general dependent type theory, i.e. the characterization that you'd want.

My point is really that you can at least characterize his object without reference to the other. I doubt that in MLTT you can define the sum in terms of the product, but the characterization doesn't care anyway.
One softer variation of your question for me would then be: What do theories look like that only have one and not the other.

Granted, I never restricted myself in that way. My gripple with homotopy type theory etc. is that the fancy models of equality never seem to make for useable normal-adga like frameworks, do they?

Oh and one thing that seems to have changed totally in 2017 is the hardness of the image Captchas. It's super annoying. It comes down to making educated guesses of what the machine learning tool recognizes and what not