文献

J-GLOBAL ID：202202261529940051   整理番号：22A0691464

ホモトピー型理論における歩行と球面写像のホモトピーについて【JST・京大機械翻訳】

On homotopy of walks and spherical maps in homotopy type theory

著者 (1件)： Prieto-Cubides Jonathan (University of Bergen, Norway)
資料名： ACM Proceedings  (ACM Proceedings)
号： CPP 2022  ページ： 338-351  発行年： 2022年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： コンビナトリアルマップを用いて,耳石までの表面へのグラフ埋込みを表現した。グラフを埋め込む表面は,このアプローチに陰的である。ここでの建設は,証明関連であり,ホモトピー型理論の言語の部分集合で記述される。本論文は,離散ノード集合を有する接続および有向マルチグラフの球面マップと呼ばれる球における埋込みの1つの特性評価の精密化を提示した。歩行のためのホモトピーのコンビナトリアル概念と還元関係の下での歩行の正常形式を紹介した。球面マップ状態の最初の特性化は,同じ終点を持つ歩行の対が単に歩行-ホモトピックであるならば,グラフを球に埋め込むことができる。この定義の精密化は,内部サイクルによる歩行を除外した。離散ノード集合を持つグラフに対して球面マップが与えられるならば,この補助定理の1つにおいて証明されるように,グラフにおける任意の歩行は,通常形式に対して単にウォーク-ホモトピックである。証明支援Agdaは,本論文で記録された結果の形式化に寄与した。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： グラフ ,  *写像 ,  言語 ,  地図 ,  *ホモトピー ,  集合 ,  平衡石 ,  球面 ,  精密化 ,  部分集合 ,  キャラクタリゼーション ,  埋込み【写像】 ,  *型理論
準シソーラス用語： エンドポイント ,  補題 , 【Automatic Indexing@JST】

著者キーワード (4件)： Agda ,  HoTT ,  グラフマップ ,  歩行正規形

分類 (2件)： 代数学  (AB02000R) ,  グラフ理論基礎  (IA02020S)

タイトルに関連する用語 (5件)： ホモトピー ,  型理論 ,  歩行 ,  球面 ,  写像