Seminar za matematičku logiku i osnove matematike

lokacija: 
PMF Matematički odsjek (virtualno)
vrijeme: 
25.05.2020 - 17:00 - 19:00

Na Seminaru za matematičku logiku i osnove matematike, u ponedjeljak 25. svibnja 2020. u 17 sati,

Vedran Čačić će održati predavanje

Calculus of inductive constructions (3)
 
Sažetak: U trećem dijelu, još ćemo malo pričati o distinkciji između rekurzivnosti i rekurzivne prebrojivosti, odnosno između računanja (koje je sasvim automatizabilno, i uvijek stane) i dokazivanja (koje je vođeno ljudskom rukom, i stane ako je dokaz pronađen). Za primjer ćemo dokazati jedno svojstvo Ackermannove funkcije, čija rekurzija nije toliko jednostavna da bismo njeno računanje mogli sasvim automatizirati u Coqu, ali će "vođeni" dokaz biti prilično jednostavan.
Ako ostane vremena, reprezentirat ćemo jednostavni kompajler (stabala aritmetičkih izraza u jezik nekog virtualnog stroja sa stogom) i dokazati njegovu korektnost.
 
Tko se želi okušati do ponedjeljka, zadatak je sljedeći: A3 je "generalizirana aritmetička operacija": A3(x,y,z) je sljedbenik od y za z=0, zbroj x i y za z=1, umnožak xy za z=2, potencija za z=3, tetracija za z=4 itd. S druge strane, A2 je ona "uobičajena" Ackermannova funkcija (koja uopće nije Ackermannova već Peter—Robinsonova). Treba dokazati A2(m,n)+3=A3(2,n+3,m).
 
Seminar će se održati putem Zoom-a. Link i potrebni podaci su ovdje (isti kao prošli put):
 
Ako nemate klijentski program za Zoom, možete ga besplatno skinuti ovdje:
 
 

Snimka prošlog seminara: https://meduza.carnet.hr/index.php/media/watch/16658

Share this