2023/09/07(木)のゾンビ論文 依存型プログラミング言語Zombie Trellysって何だれかおしえて
ゾンビについて書かれた論文を収集すべく、Googleスカラーのアラート機能を使っている。アラート設定ごとに、得られた論文を以下にまとめる。
アラートの条件は次の通り。
「zombie -firm -philosophical -botnet -xylazine -biolegend -gender」
「zombie -firm -philosophical -DDoS -xylazine -viability -gender」
「zombie -firm -philosophical -DDoS -xylazine -biolegend -gender」
「zombie -firm -philosophical」（取りこぼし確認）
「zombie -firm -consciousness」（取りこぼし確認その2）
検索条件は次の意図をもって設定してある。
「zombie」：ゾンビ論文を探す
「-firm」：ゾンビ企業を扱う経済学の論文を排除する
「-philosophical」/「-consciousness」：哲学的ゾンビを扱う哲学の論文を排除する
「-DDoS」/「-botnet」：ゾンビPCを扱う情報科学の論文を排除する
「-xylazine」：ゾンビドラッグに関する論文を排除する
「-viability」/「-biolegend」：細胞の生死を確認するゾンビ試薬を使う医学の論文を排除する
「-gender」：ジェンダー学の論文を排除する
また、検索条件4と5では、上記の検索キーワードで不必要にゾンビ論文を排除していないかを確かめる。
今回、それぞれのヒット数は以下の通り。
「zombie -firm -philosophical -botnett -xylazine -biolegend -gender」二件
「zombie -firm -philosophical -DDoS -xylazine -viability -gender」二件
「zombie -firm -philosophical -DDoS -xylazine -biolegend -gender」二件
「zombie -firm -philosophical」二件（差分ゼロ件）
「zombie -firm -consciousness」二件（条件4との差分ゼロ件）
検索条件1-3は評論、情報科学が一件ずつだった。
検索条件1「zombie -firm -philosophical -botnet -xylazine -biolegend -gender」
書評：ジョナサン・チャーテリス＝ブラック、コロナウイルスのメタファー：見えない敵か、それともゾンビの黙示録か？
一件目。
原題：Book review: Jonathan Charteris-Black, Metaphors of Coronavirus: Invisible Enemy or Zombie Apocalypse?
掲載：Discourse & Society
著者：Julia T. Williams Camus
ジャンル：評論
Jonathan Charteris-Black著の『Metaphors of Coronavirus: Invisible Enemy or Zombie Apocalypse?』は以前にゾンビ論文のひとつとして触れたことがある。その時の私の解説を引用しておく。
論点の中心にあるのは、ゾンビ・アポカリプスと‘We are the virus’ meme（「私たちはウイルス」ミーム）。ゾンビ・アポカリプスの説明は不要だと思うが、後者は端的に言えば、人間がコロナに感染してその数を減らすことで地球環境が改善する、つまり人間が地球にとってのウイルスであるとする考え方のこと。
この2つがコロナ禍においてなぜ流行ったのか（たぶん、アメリカで流行ったのだろう）を読み解く、というものらしい。
というのが、『Metaphors of Coronavirus: Invisible Enemy or Zombie Apocalypse?』に関する私の理解だ。
今回見つけた論文はこれに関する書評だということだから、私よりもずっと詳しい解説が書かれているのだろう。しかし、アブストラクトやまとめにすらアクセスできないため、何に着目しているのかまるでわからない。
とりあえず、ジャンルは評論。
論理等価性リフレクションを使用した依存型プログラミング
二件目。
原題：Dependently-Typed Programming with Logical Equality Reflection
掲載：Proceedings of the ACM on Programming Languages, 2023
著者：Yiyun LiuとStephanie Weirich
ジャンル：情報科学
zombieの単語は"Zombie Trellys system"という文字列で出てくる。どうやら「依存型言語」という種類のプログラミング言語があり、依存型言語にTrellys名前の言語があり、それを発展させるプロジェクトがペンシルバニア大学の工学部主導？で動いていたらしく、その成果物のひとつが"Zombie Trellys"らしい。
まず、依存型の説明をWikipediaから引用する。意味はわからないが。
依存型 (いぞんがた、英: dependent type) とは、計算機科学と論理学において、値に依存する型のことである。数学の型理論の表現形式と計算機科学における型システムの特徴を併せ持つ。直観主義型理論においては、全称量化子や存在量化子のような論理学における量化子をエンコードするために依存型が用いられている。ATS（英語版）、Agda、Idris（英語版）、Epigram（英語版）などのいくつかの関数型プログラミング言語では、依存型を使った非常に表現力の強い型によって、バグを防止している。
次に、Trellysについて日本語で書いてある唯一の文献を引用する。これもやはり意味が分からない。
依存型プログラミング言語は，不変量を型としてコー ド化することによって，検証とプログラミングを統 合化するメカニズムを備えている．従来，依存型言語は型理論に基づくもので，証明とプログラムの間の直接的な関係はカリー・ハワード同型対応を基礎としていた．しかし，この対応関係では，論理的な安定性を確保するために言語を正規化する必要があ るので，それなりの代償が強いられるものだった． Trellysは現在開発中の値呼びによる依存型プログラミング言語で，型理論と，一般再帰，Type: Type，および任意のデータ型を含む不安定なプログラム機能を統合化するように設計されている．本論文では， Trellys用の 1 つのコア言語設計の概要を説明する とともに，発散の可能性があるプログラムについて 安定した推論を促進する重要な言語構成要素の使用法を示す．
Progress in Informatics
『Equational reasoning about programs with general recursion and call-by-value semantics』
アブストラクトより
最後に、Zombie Trellysは次の論文で初めに提案？言及？されたらしい。
https://dl.acm.org/doi/10.1145/2535838.2535883
一応Zombie Trellysを発展した順に追ってみたが、何もわからない。
ところで、掲載誌であるProceedingsを発行しているACMは何度か見た記憶がある。自分の記事を検索したところ、過去に三回触れていたようだ。三回程度ならば検索キーワードを設定して排除するまでもない。次からは「Proceedings of the ACM」という文字列が見えたらもうその論文を読むのはやめにしよう。疲れてしまった。
ジャンルは情報科学。
検索条件1-3の差分（差分なし）
「DDoS/botnet」と「viability/biolegend」で検索結果に差異が生じるか調べる。
今回は差分がなかった。
検索条件4「zombie -firm -philosophical」（差分なし）
上記の条件で誤ってねらいのゾンビ論文を取りこぼしていないかチェックするために、こちらの検索結果もチェックしておく。ただし、ゾンビ企業と哲学的ゾンビは意図的に取りこぼすこととする。
条件1-3との差分はなかった。
検索条件5「zombie -firm -consciousness」（差分なし）
「zombie -firm -philosophical」との差分を確認する。哲学的ゾンビのみを排除するには「-philosphical」（哲学的な）と「-cousciousness」（意識）のどちらが良いかを探る目的。前者は哲学的ゾンビが英語でphilosophical zombieとつづることから、後者は哲学的ゾンビが人間の意識の有無に注目した概念であることから、それぞれ排除可能。
今回は差分がなかった。
まとめ
検索条件1-3は医学、言語学が一件ずつだった。
特に適した理由もなく、おそらく憎悪を煽る目的でゾンビの比喩が使われる例を今日初めて知った。以前にアルツハイマーや認知症の患者がゾンビに喩えられることで結果として偏見が生まれると警告する論文を見たことがあるが、それは、言いたくはないが、おそらく患者の言動や見た目がゾンビに似ているからだ。
ただ、そうではなく、ゾンビに喩えるだけの確かな理由があるのかもしれない。今回の論文を読んだだけではわからなかったが。
今日はねらいのゾンビ論文なし。
#Zombie -Trellys