-
- いいね！0
Keigo Imai
@keigoi
Rの十分完全性 <=> 任意の基底項s_gに対して，基底構成子t_gが存在して s_g =>R t_g. 目的：条件付き項書き換えシステムの解明に適した枠組みをつくる。 (良く分かっていない…) CTRS を TRS に変換：アンラベリング変換 (条件部分に相当する新しい関数記号を導入して更に重複を省く(deterministicに
2019-06-07 09:43:02
よんた
@keita44_f4
#IPSJPRO CTRSのアンラベリング変換、true/false程度の条件なら有限のルール変換でできるけど、不等号みたいなのは取り扱えない気がする。そもそもCTRSには不等号が禁止されているとか？
2019-06-07 09:43:44
Keigo Imai
@keigoi
3DCTRS ∀ l -> r <= c in R について 3型: V(r) ⊆ V(l) ∪ V(c) D: determinisitc 指向式: (...) let 文のようなものをモデル化できるほか、アンラベリングにも適している #IPSJPRO
2019-06-07 10:00:56
Keigo Imai
@keigoi
2019-1-(5)：10:00-10:30（短い発表） 「項書き換えシステムにおける局所十分完全性の証明法の提案」 ○白石 智輝, 青戸 等人 (新潟大学大学院自然科学研究科)
2019-06-07 10:01:20
Keigo Imai
@keigoi
局所十分完全: 代入後の基底項が基底構成子項に書き換えできること. （全ての項に対してそのような代入があること？） #IPSJPRO (ツイートしてると置いていかれる。
2019-06-07 10:16:05
Keigo Imai
@keigoi
2019-1-(6)：10:30-11:00（短い発表） 「条件付き項書き換えシステムの階層合流性証明法」 ○加賀谷 有輝, 青戸 等人 (新潟大学大学院 自然科学研究科) #IPSJPRO
2019-06-07 10:37:17
Keigo Imai
@keigoi
#IPSJPRO 2019-1-(7)：11:15-12:00 「An extended SECD machine with a first-class macro mechanism」 ○福田 陽介 (京都大学情報学研究科) 実装は以下にあります： github.com/yf-fyf/hlisp
2019-06-07 11:05:25
Keigo Imai
@keigoi
#IPSJPRO 条件式, 再帰関数, quasi-quote の言語機能を HLisp 自身で定義できる．{Landin, '64] の SECD機械の拡張でできている．必要最小限の操作的意味論とはどのようなものか，という興味に基づいている． twitter.com/keigoi/status/…
2019-06-07 11:16:45
Keigo Imai
@keigoi
#IPSJPRO ライブコーディング！の後に，if文の「定義」 ここ： github.com/yf-fyf/hlisp/b…
2019-06-07 11:21:52
Keigo Imai
@keigoi
#IPSJPRO 普通のクロージャ (lambda (args) body) とおなじように，マクロクロージャ (macro (args) body) が定義できる． twitter.com/keigoi/status/…
2019-06-07 11:23:31
Keigo Imai
@keigoi
#IPSJPRO [Plotkin '75] の流れをフォローします. 操作的意味論. evaluation context で引数部分にちょっとside condition がある (関数部分がマクロのとき引数を評価しないように)．twitter.com/keigoi/status/…
2019-06-07 11:28:57
Keigo Imai
@keigoi
#IPSJPRO (拡張) SECD machine． 先ほどの calculus とは value の定義がちょっと違う (明示的にクロージャをλと環境の対でもつ). 状態 <S,E,C,D>: stack, environment, control string, dump. やはり関数部分が関数かマクロかを見る．引数のスタックへの積み方が変わる． twitter.com/keigoi/status/…
2019-06-07 11:37:45