From 5c45dba816ff6e75fd3426f78b4cfe7e74082a6f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E6=9D=BE=E6=B5=A6=20=E7=9F=A5=E4=B9=9F=20Matsuura=20Tomoy?= =?UTF-8?q?a?= Date: Wed, 22 Nov 2023 11:32:45 +0900 Subject: [PATCH] [obsidian] vault backup: 2023-11-22 11:32:45[ --- content/mimium新内部表現の構想.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/content/mimium新内部表現の構想.md b/content/mimium新内部表現の構想.md index 65229360..2ab66f1b 100644 --- a/content/mimium新内部表現の構想.md +++ b/content/mimium新内部表現の構想.md @@ -48,9 +48,10 @@ $$ \begin{align} e \; ::=& \quad x \quad x \in \mathbb{V} \quad & [value]\\ |& \quad \lambda x.e \quad & [lambda]\\ - |& \quad fix \; x.e \quad & [fix]\\ - |& \quad feed \; x.e \quad & [feed] \\ + |& \quad fix \; x.e \quad & [fixpoint]\\ |& \quad e \; e \quad & [app]\\ + |& \quad feed \; x.e \quad & [feed] \\ +|& \quad delay \; e \; e & [delay]\\ %%|& \quad (e_1,e_2) \quad & [product]\\ %%|& \quad \pi_n e \quad n\in \mathbb{N},\; n>0 \quad & [project]\\ %%|& \quad \langle e \rangle \quad & [code] \\ @@ -223,8 +224,9 @@ $$ でラムダ抽象とFeedの型付け規則こういう感じになると $$ -\frac{\Gamma, x:\tau^a \vdash e:\tau^b}{\Gamma \vdash \lambda x.e:\tau^a \to \tau^b }\\ -\\ +\frac{\Gamma, x:\tau^a \vdash e:\tau^b}{\Gamma \vdash \lambda x.e:\tau^a \to \tau^b } +$$ +$$ \frac{\Gamma, x : \tau_p^a \vdash e: \tau_p^a }{\Gamma \vdash feed\ x.e:\tau_p^a} $$