Una verifica formale delle Permutazioni Primitive Reversibili

Proof assistants are computer programs designed to help with the development of formal proofs. In this thesis we explore this topic using the Lean theorem prover, and by formalizing an article on reversible computing - specifically, about a class of invertible computable functions called Recursive Primitive Per- mutations which are expressive enough to encode the whole class of Primitive Recursive Functions. In doing so, many aspects of the original paper are re- elaborated and simplified, like the definition, the construction of the Cantor pairing and the proof of PRF-completeness.

I proof assistant sono programmi informatici utilizzati per lo sviluppo di dimostrazioni formali. In questa tesi esploriamo questo argomento usando il Lean theorem prover, e formalizzando un articolo sulla computazione reversibile - in particolare, su una classe di funzioni chiamate Permutazioni Primitive Reversibili che sono abbastanza espressive da poter codificare l'intera classe delle Funzioni Primitive Ricorsive. Molti aspetti del paper originale sono rielaborati e semplificati, come la definizione, la costruzione del Cantor pairing e la dimostrazione della PRF-completezza.