From a1c8741be5ab09eb20399a66cabb88a827c351bd Mon Sep 17 00:00:00 2001 From: acondolu Date: Tue, 29 May 2018 18:40:06 +0200 Subject: [PATCH] Fixes --- ac_notes.tex | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/ac_notes.tex b/ac_notes.tex index aa11df8..498812e 100644 --- a/ac_notes.tex +++ b/ac_notes.tex @@ -13,27 +13,29 @@ \maketitle +\newcommand{\Prgm}[2]{[#1\Comma #2]} + \subparagraph{Syntax} \[\begin{array}{lll} - \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \tm\Semi\vec\tm \\ - n & \ddef & \Lam\var n \Semi \vec n \mid \var\,\vec n \\ + \tm, \tmtwo & \ddef & \var \mid \tm\,\tmtwo \mid \Lam\var \Prgm{\tm}{\vec\tm} \\ + n & \ddef & \Lam\var \Prgm{n}{\vec n} \mid \var\,\vec n \\ \\ C & \ddef & \Box \mid C\,\tm \mid \tm\,C \\ - P & \ddef & \Box \Semi \vec\tm \mid C[\Lam\var P] \Semi \vec\tm \\ - \tilde P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm \\ + P & \ddef & \vec\tm \Comma \Box \Comma \vec\tm \mid \vec\tm \Comma C[\Lam\var P] \Comma \vec\tm \\ \end{array}\] \subparagraph{Reduction} \[\begin{array}{lll} - P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\in \tm\Comma\vec\tm} & - P[C[\tm\Subst\var\tmtwo], \vec\tm\Subst\var\tmtwo]\\ - P[C[(\Lam\var \tm\Semi\vec\tm)\,\tmtwo]] & \Red{}{\var\not\in\tm\Comma\vec\tm} & - P[C[\tm] \Semi \vec\tm\Comma\tmtwo]\\ + P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\in \Prgm\tm{\vec\tm}} & + P[C[\tm\Subst\var\tmtwo]\Comma \vec\tm\Subst\var\tmtwo]\\ + P[C[(\Lam\var \Prgm\tm{\vec\tm})\,\tmtwo]] & \Red{}{\var\not\in\Prgm\tm{\vec\tm}} & + P[C[\tm] \Comma \vec\tm\Comma\tmtwo]\\ \end{array}\] \subparagraph{Properties of the calculus:} \begin{itemize} \item Every term is normalizing iff it is strongly normalizing. + \item Ogni strategia e' perpetua! \end{itemize} \clearpage -- 2.39.2