Učitavanje video playera...
00:57:44
Vedran Čačić: 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).
Objavljeno: 28.05.2020
Unutar kategorije: Obrazovanje

Srodni zapisi