Cosa fare e come consegnare

Scaricate il file exercise-structural.ma (usando il pulsante destro sul link e selezionando Save link as' o qualcosa di simile). Poi aprite il file salvato lanciando un terminale e lanciando il comando~sacerdot/matita_gtk3/helm/matita/matita/matita.opt exercise-structural.ma' dalla directory in cui l'avete salvato.

Per prima cosa all'inizio del file riempite i campi con i vostri nomi, cognomi e numero di matricole.

Durante la prova ricordatevi di salvare costantemente per non perdere il lavoro in caso di crash. Matita fa dei salvataggi automatici, ma non fidatevi.

Alla fine dell'esercitazione o del tempo consegnate il file con il comando `~sacerdot/logica1920/ConsegnaLogica exercise-structural.ma'.

Come scrivere i simboli

Per inserire i simboli matematici è necessario digitare il loro nome e poi premere ALT-L. In generale i nomi dei simboli sono della forma \nome, ad esempio \equiv. Alcuni simboli molto frequenti hanno dei sinonimi più comodi da digitare, per esemio ⇒ ha sia il nome \Rightarrow sia =>.

Segue un elenco dei simboli più comuni e i loro nomi separati da virgola, Se sono necessari dei simboli non riportati di seguito si può visualizzare l'intera lista dal menù a tendina View ▹ TeX/UTF8 table.

• → : \to, ->
• ⇒ : \Rightarrow, =>
• ℕ : \naturals (o anche semplicemente N seguito da ALT-L)
• ≝ : \def, :=
• ≡ : \equiv
• ∀ : \forall

La sintassi ℕ → ℕ è il tipo delle funzioni unarie che preso un numero naturale restituiscono un numero naturale.

→ associa a destra. Pertanto ℕ → ℕ → ℕ è da leggersi come ℕ → (ℕ → ℕ), ovvero il tipo delle funzioni che preso un primo input restituiscono una funzione che preso un secondo input restituiscono un naturale. In altre parole, ℕ → ℕ → ℕ è il tipo delle funzioni binarie sui naturali.

La sintassi di Matita

Il linguaggio di Matita si basa sul λ-calcolo CIC, la cui sintassi si differenzia in vari aspetti da quella che solitamente viene utilizzata per fare matematica e si avvicina a quella dei più noti linguaggi di programmazione funzionale.

La sintassi dei termini (o espressioni) è grosso modo generata dalla seguente BNF:

T ::= x | y | pippo | Pluto | ... variabili e costanti (sequenze di maiuscole, minuscole, numeri) | T ... T applicazione prefissa | T SIMBOLO T applicazione infissa dove SIMBOLO è un simbolo come +, -, =, etc. | λx.T una funzione che prende in input la variabile x (o y, o z, etc.) e restituisce in output T

• applicazione prefissa

  Se f è una funzione che si aspetta due argomenti, l'applucazione di f agli argomenti x e y si scrive (f x y) e non f(x,y). Le parentesi possono essere omesse se il senso è chiaro dal contesto. Similmente, l'applicazione di una funzione unaria a x si scrive semplicemente f x.

• applicazioni infisse

  L'applicazione dell'uguaglianza a x e a f z si scrive semplicemente x + f z (da leggersi come x + (f z)). Similmente per gli altri simboli infissi.

Un file matita è una sequenza di dichiarazioni di tipo, definizioni di funzione, definizione di funzioni per ricorsione strutturale, assiomi e teoremi.

• Per dare la definizione ricorsiva (di un linguaggio) si definisce un tipo di dato ricorsivo (detto induttivo) che ne cattura l'albero di sintassi astratta. Le dichiarazioni induttive usano una sintassi simile a BNF. Per esempio per definire

  <A> ::= <A> "+" <A> | <A> "*" <A> | "-" <A> | "0" | "1"
  

  si usa il seguente comando

  inductive A : Type ≝
  | Plus : A → A → A    
  | Times : A → A → A
  | Minus : A → A
  | Zero : A
  | One : A
  .
  

La ratio è che Plus prende due argomenti di tipo A per darmi un A, pertanto il simbolo terminale Plus è assimilabile a una "funzione" binaria di tipo A → A → A. Essa, tuttavia, non è una vera funzione ma solamente un terminale in quanto non calcola nulla. Matita capisce che è un terminale (chiamato costruttore) in quanto è definito come uno dei casi del tipo induttivo A nella definizione di A.

Analogamente Minus prende un argomento di tipo A per dare un A ed è pertanto dichiarato di tipo A → A. Zero e One sono invece simboli terminali atomici: essi non hanno argomento e sono già di tipo A. Vengono pertanto dichiarati come avente tipo A.

Plus, Times, Minus non sono simboli infissi. Pertanto si utilizza la normale sintassi per l'applicazione. Per esempio, 0 + -1 * 0 va scritto come Plus Zero (Times (Minus One) Zero).

• Le funzioni definite per ricorsione strutturale utilizzano il costrutto let rec (ricorsione) e il costrutto match (analisi per casi).

  Ad esempio la funzione count definita nella sintassi vista a lezione come

  count Zero = 1
  count (Minus F) = 1 + count F
  count (Times F1 F2) = 1 + count F1 + count F2 
  ...
  

  la si esprime come

  let rec count F on F ≝ 
    match F with 
    [ Zero ⇒ 1 
    | Minus F ⇒ 1 + count F
    | Times F1 F2 ⇒ 1 + count F1 + count F2 
    ...
    ].
  

  da leggersi come

  • sto definendo una funzione per ricorsione strutturale (let rec)
  • il nome della funzione è count e prende un solo input F (count F)
  • la funzione è per ricorsione sul primo (e unico) input (on F)
  • la funzione va per casi sulla forma di F (match F with)
  • ognuno dei casi deve considerare una produzione; il pattern e l'output vengono separati da ⇒. Esempio: nel caso Times F1 F2 l'output è 1 + count F1 + count F2. F1 e F2 sono i parametri formali (i non terminali)
  • valgono le normali regole della ricorsione strutturale: ogni produzione deve essere considerata esattamente una volta e tutte le chiamate ricorsive debbono essere sui parametri formali