pandaman pandaman64

旧石器時代のポインタをご利用の皆様へ～provenance入門～

現代のプログラミング言語ではポインタは単なるアドレスではなく，provenanceを伴った参照として扱われています．知識をアップデートしましょう．

Lee, Hur, Jung, Liu, Regehr, Lopes.

低レベル言語（C, C++, Rust）のコンパイラのメモリモデルには二つの相反する目標がある
- high-level optimization
  - 最適化したい
例:

	inductive Balance: Nat -> Nat -> Nat -> Type where
	\| lefty : Balance n.succ n.succ.succ n
	\| mid : Balance n n.succ n
	\| righty: Balance n n.succ.succ n.succ

	inductive Tree (a: Type u): Nat -> Type u where
	\| leaf: Tree a 0
	\| node: Balance l n r -> Tree a l -> a -> Tree a r-> Tree a n

	theory Euclid
	imports Main "HOL-Library.Disjoint_Sets"
	begin

	fun prime :: "nat ⇒ bool" where
	"prime n ⟷ n ≥ 2 ∧ (∀k ≤ n. k dvd n ⟶ k = 1 ∨ k = n)"

	lemma "prime 5"
	by code_simp

	theory Scratch
	imports Main
	begin

	lemma
	fixes m n
	assumes "m ≥ 2" "n ≥ 2"
	shows "coprime m n ⟷ (∃a b. a * int m + b * int n = 1)"
	proof
	let ?A = "{1..n}"

	<!DOCTYPE html>
	<html xmlns="http://www.w3.org/1999/xhtml">
	<head>
	<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
	<title>Theory Pumping (Isabelle2020: April 2020)</title>
	<link media="all" rel="stylesheet" type="text/css" href="isabelle.css"/>
	</head>

	<body>
	<div class="head"><h1>Theory Pumping</h1>

	Let's call (r_i)_{i>=0} the sequence of the ranks of (A^i)_{i>=0}.
	For any i>=0, the image of A^{i+1} is a subspace of the image of A^{i}.
	Our sequence of ranks (r_i) is non-increasing.

	Since Im(A^{i+1}) ⊂ Im(A^i), if there exists i such that r_i = r_{i+1}, Im(A^{i+1}) = Im(A^i).
	From this, it follows that Im(A^k) = Im(A^i) (k > i), or r_k = r_i.

	In other words, (r_i) is a sequence of non-negative integers that
	- starts at n
	- might be stricly decreasing for a while