/home/laney/.irssi/irclogs/Freenode/#agda.log-20170620

--- Day changed Mon Jun 19 2017
Nik05What are some cool things to do as a beginner?19/06 01:12
Nik05My math background is just Calculus 1, 2, Linear Algebra 1, Complex Calculus, I guess that's it19/06 01:13
Nik05And I know basic Predicate logic19/06 01:14
--- Log opened Mon Jun 19 09:04:11 2017
-!- Irssi: #agda: Total of 111 nicks [0 ops, 0 halfops, 0 voices, 111 normal]19/06 09:04
-!- Irssi: Join to #agda was synced in 108 secs19/06 09:05
--- Log closed Mon Jun 19 09:49:10 2017
--- Log opened Mon Jun 19 09:49:24 2017
-!- Irssi: #agda: Total of 114 nicks [0 ops, 0 halfops, 0 voices, 114 normal]19/06 09:49
-!- Irssi: Join to #agda was synced in 114 secs19/06 09:51
Nik05{AS} interesting things to learn more aboit agda19/06 11:44
Nik05I will check out freek19/06 11:45
{AS}Nik05: there is a book on Agda (by Aaron Stump I believe)?19/06 11:46
comietekNik05: check out http://oxij.org/note/ReinventingFormalLogic/19/06 11:51
comietekNik05: take a paper and reimplement it19/06 11:51
Nik05thank you {AS} and comietek, you guys are so helpful19/06 12:03
{AS}sure :)19/06 12:06
comietekyou're welcome19/06 12:56
Nik05comietek I will learn something new, I have no idea what the deduction theorem or implication introduction axioms are19/06 13:06
Nik05to me they just look like (A -> B) -> (A -> B) ...19/06 13:07
comietekthe deduction theorem is meaningful in a Hilbert-style formalisation19/06 13:10
comietekin a Gentzen-style (natural deduction) formalisation, the deduction theorem is the implication introduction rule, lambda19/06 13:10
comietekHilbert-style is also known as axiomatic19/06 13:10
comietekhttps://mietek.github.io/hilbert-gentzen/html/BasicIPC.Syntax.Hilbert.html#146919/06 13:11
comietekhere's how I did it, for a system extended with simple products19/06 13:11
comietekbut I was following the tutorial I linked earlier19/06 13:12
comietekNik05: you should also check out http://purelytheoretical.com/sywtltt.html19/06 13:13
comietekNik05: there is a short tutorial PDF linked from the page19/06 13:13
comietekNik05: it was very helpful for me to understand things19/06 13:13
Nik05Thank you very much, I have some reading to do19/06 13:14
Nik05comietek the pdf you mentioned, is that A Tutorial on the Curry-Howard Correspondence?19/06 13:16
comietekNik05: yes19/06 13:16
comietekNik05: the other advice on that page is also pretty good19/06 13:16
comietekNik05: especially about lectures by Frank Pfenning19/06 13:16
Nik05Are those lecture accessable for non mathematicians?19/06 13:17
comietekhttp://www.cs.cmu.edu/~fp/courses/15317-f09/schedule.html19/06 13:17
comietekthese are intro-level lectures for students19/06 13:17
Nik05oke19/06 13:17
comietekI learned a lot by following them, and I would recommend them19/06 13:17
comietekhttp://www.cs.cmu.edu/~fp/courses/15816-s10/schedule.html19/06 13:17
comietekI should go through them again, because I'm sure there's more to learn19/06 13:17
comietekthey are very well written19/06 13:18
Nik05And Modal Logic, havent been able to read about that yet19/06 13:18
comietekand there are also videos on the summer school site19/06 13:18
comietekthere is a link to the most important set of videos on the page I pasted earlier19/06 13:18
comietekbut the OPLSS lectures go back 10 years19/06 13:18
comietekif you like watching videos, there's a lot of good material19/06 13:19
Nik05What do you recommend to start with?19/06 13:20
Nik05Proof Theory Foundations?19/06 13:21
comietekyes19/06 13:21
comietekthat should go hand in hand with the lecture notes for the constructive logic course19/06 13:21
comietekOPLSS 201219/06 13:22
Nik05Oke, thank you19/06 13:22
comietekbut I would actually read that PDF first19/06 13:22
comietekit's short and to the point19/06 13:22
Nik05Your library is huge. How do you keep track of all the symbols you used?19/06 13:33
comietekNik05: I assign them methodically19/06 13:38
comietekbut that's old code anyway19/06 13:38
comietekI also continuously rewrite things19/06 13:38
comietekso that's one way to keep them in mind19/06 13:38
comietek:)19/06 13:38
comietekNik05: the entry point to browse things is https://mietek.github.io/hilbert-gentzen/html/Everything.html in case you haven't figured that out yet19/06 13:40
comietekNik05: but you shouldn't worry about this yet19/06 13:40
Nik05Already saw it :P19/06 13:40
comietekNik05: the other things will be much better reading19/06 13:40
Nik05Oh I don't worry, I was just interesting19/06 13:40
Nik05it*19/06 13:41
comietekNik05: https://mietek.github.io/imla2017/html/Everything.html is more modern and focused19/06 13:41
Nik05Downloaded a few GB's of lectures :)19/06 13:43
Nik05first half hour is already 1.7GB :P19/06 13:43
comietekgood quality19/06 13:43
comietekif only they could stop switching the audio source...19/06 13:43
comietekthere's a delay of about 1s every time they switch19/06 13:44
Nik05They do that alot in lectures...19/06 13:44
Nik05And each source is on another ear 19/06 13:44
Nik05comietek why would you define a function with one argument as infix?19/06 14:14
comietekNik05: prefix/postfix?19/06 14:14
Nik05yes19/06 14:15
comietekAgda doesn't have a keyword "prefix" or "postfix"19/06 14:15
Nik05What is the difference between a prefix and a "normal" function?19/06 14:15
comietekjust syntax sugar19/06 14:15
comietekfewer parentheses sometimes19/06 14:15
Nik05the default precendence is different?19/06 14:16
Nik05or is it that you can specify the precendence of prefixes and not of functions19/06 14:16
comietekyes, by default function application binds with the higher precedence, I think19/06 14:16
Nik05oh oke19/06 14:16
comietekhighest*19/06 14:16

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!