訳語一覧（英→日バージョン）

[keiichirou shikano]

『型システム入門』の翻訳時に共有していた、型システムに関する英語表現の訳語一覧です。

as-isで恐縮ですが役に立つかもしれないので流します。

Church encoding	Church表現
Church numeral	Church数
Church-style	Churchスタイル
Curry-Howard correspondence	Curry-Howard対応
Curry-style	Curryスタイル
Extended Static Checking	拡張静的検査
F-bounded quantification	F有界量化
F-closed	閉じている（生成関数Fについて）
F-consistent	整合的（生成関数Fについて）
F-ground	基底（生成関数Fの）
F-supported	支持されている（生成関数Fに）
ML-style polymorphism	ML式多相
Y-combinator	Yコンビネータ
abbreviation	省略/略記
abbreviation	略記/省略
abstract data type (ADT)	抽象データ型
abstract machine	抽象機械
abstract syntax tree	抽象構文木
abstract syntax	抽象構文
abstraction boundary	抽象境界
abstraction	抽象/抽象化
activation record	起動記録
actual parameter	実引数
ad-hoc polymorphism	アドホック多相
algorithmic subtyping relation	アルゴリズム的部分型関係
algorithmic subtyping	アルゴリズム的部分型付け
algorithmic typing relation	アルゴリズム的型付け関係
algorithmic typing	アルゴリズム的型付け
alias analysis	別名解析
aliasing	別名付け
allocation	確保（参照の/記憶域の）
alpha-conversion	アルファ変換
antisymmetric	反対称的
arithmetic expression	算術式
arithmetic	算術
array-bounds checking	境界検査（配列の）
arrow type	矢印型
assignment	破壊的代入
associativity	結合規則
assumption	仮定
atomic type	原子型
axiom	公理
axiomatic semantics	公理的意味論
base type	基本型
behaviorally equivalent	振る舞い等価
beta-reduction	ベータ簡約
big-step evaluation	大ステップ評価
big-step operational semantics	大ステップ操作的意味論
binary operation	二項演算
binary relation	二項関係
binder	束縛子
bisimulation	双模倣性
boolean	ブール値
bound	束縛
bounded below	下に有界
bounded existentials	有界存在型
bounded quantification	有界量化
bounded quantifier	有界量化子
bounded type operator	有界型演算子
bounded universals	有界全称型
boxed	ボックス化された
call by name	名前呼び
call by need	必要呼び
call by value	値呼び
canonical form	標準形
capture-avoiding substitution	捕獲回避代入
cartesian product	デカルト積
cast(ing)	キャスト
categorial grammar	範疇文法
category theory	圏論
channel type	チャネル型
class	クラス
closed	閉じている（項が）
closure property	閉包性
coercion	型強制
coherence	整合性
coinduction	余帰納法
colored local type inference	色付き局所型推論
combinator	コンビネータ
combinatory logic	コンビネータ論理
complete induction	完全帰納法
complete	完全
completely bounded quantification	完全有界量化
compositionality	合成性
compound type	複合的な型
comprehension notation	内包表記
computation rule	計算規則
computational effect	計算的作用
concrete syntax	具象構文
conditional (expression)	条件式
confluent	合流性
congruence rule	合同規則
constraint set	制約集合
constraint type	制約型
constraint typing relation	制約型付け関係
constraint typing	制約型付け
constructive logic	構成的論理
constructive type theory	構成的型理論
constructor	構築子
context	文脈
continuation	継続
contractive	縮小的
contravariant	反変
correct by construction	構成により正しい
countable	可算
covariant	共変
cumulative	累積的
currying	カリー化
cut elimination	カット除去
dangling reference	ぶら下がり参照
deallocation	解放（記憶域の）
decidable	決定可能
decision procedure	決定手続き
declarative	宣言的
decreasing chain	降下列
definitional equivalence	定義による等価性
delegation	委譲
denotational semantics	表示的意味論
dependent function type	依存関数型
dependent kind	依存カインド
dependent type	依存型
depth subtyping	深さ部分型付け
depth	深さ（項の）
dereference	参照先の値を取り出す
derivable	導出可能
derivation tree	導出木
derived form	派生形式
destructor	分解子
desugaring	脱糖衣
diamond property	ダイヤモンド性
dimension analysis	次元解析
disjoint union	直和
diverge	発散する
divergent combinator	発散コンビネータ
domain theory	領域理論
domain	定義域
don't care	何でもよい
downcast	ダウンキャスト
dynamic dispatch	動的ディスパッチ
dynamic type-testing	動的型テスト
dynamic typing	動的型付け
eager	先行的
elaboration function	詳細化関数
elimination rule	除去規則
empty set	空集合
encapsulation	カプセル化
encoding	表現
enumerated type/enumeration	列挙型
environment	環境
equational unification	等式単一化
equi-recursive	同値再帰
equivalence check	等価性検査
equivalence	同値関係
equivalent	同値
error	エラー
evaluation context	評価文脈
evaluation judgment	評価判断式
evaluation relation	評価関係
evaluation statement	評価関係式
evaluation strategy	評価戦略
evaluation	評価
exception handler	例外ハンドラ
exception	例外
excluded middle	排中律
existential quantifier	存在量化子
existential type	存在型
existential unificand	存在型被単一化子
explicit substitution	明示的代入
exposed	露出している（項が/型が）
expression	式
expressive power/expressiveness	表現力
extend	拡張する（クラスを）
extensible variant type	拡張可能バリアント型
external language	外部言語
field access	フィールド参照
finalizer	ファイナライザ
finitary overloading	有限オーバーロード
first-class citizen	一級市民
first-class polymorphism	一級多相
first-class	一級
fixed point	不動点
fixed-point combinator	不動点コンビネータ
flattened data structures	平坦化されたデータ構造
flexible tuple	柔軟な組
formal method	形式手法
formal parameter	仮引数
free variable	自由変数
free	自由（変数の出現が）
full abstraction	完全抽象
full beta-reduction	完全ベータ簡約
full subtyping rule	フル部分型付け規則
function	関数
garbage collection	ガベージコレクション
generalization	一般化（型変数の）
generating function	生成関数
generating set	生成集合
generation lemma	生成補題
genericity	総称性
generics	ジェネリクス
go wrong	おかしくなる（項が/プログラムが）
goal	ゴール
grammar	文法
greatest lower bound	下限
greedy type inference	貪欲型推論
handle	処理する（例外を）
hash consing	ハッシュコンシング
heap	ヒープ
hidden representation type	隠蔽表現型
higher-order bounded quantifiers	高階有界量化子
higher-order function	高階関数
higher-order quantification	高階量化
higher-order type operator	高階型演算子
identity function	恒等関数
ill-typed	正しく型付けされていない
impredicative polymorphism	非可述的多相
impredicative	非可述的
impure	純粋でない
induction on derivation	導出に関する帰納法
induction	帰納法
inference rule	推論規則
inheritance	継承
inject	入射
inner class	内部クラス
instance variable	インスタンス変数
instance	インスタンス
instantiate	インスタンス化する
instantiate	具体化する（型を）
intensional polymorphism	内包的多相
interface	インターフェイス
intermediate language	中間言語
internal language	内部言語
interpretation function	解釈関数
intersection type	交差型
introduction rule	導入規則
invariant	不変条件
inversion lemma	逆転補題
invertible	可逆
iso-recursive	同型再帰
isomorphic	同型
join	結び
kernel subtyping rule	カーネル部分型付け規則
kind	カインド
kinding	カインド付け
label	ラベル
lambda cube	ラムダキューブ
lambda-abstraction	ラムダ抽象
lambda-calculus	ラムダ計算
lambda-term	ラムダ項
late binding	遅延束縛
latent typing	潜在的型付け
lazy	遅延評価
least upper bound	上限
leftmost	最左
less specific	限定的でない（代入が）
let-polymorphism	let多相
lexical analyzer	字句解析器
lexical scope	レキシカルスコープ
lexicographic induction	辞書式帰納法
lexicographic order	辞書式順序
lightweight formal method	軽量形式手法
linear logic	線形論理
linking	リンク（モジュールの）
local type inference	局所型推論
local type reconstruction	局所型再構築
location	位置（ストアでの）
logical predicate	論理述語
logical relation	論理関係
map	写す
mapping	写像
marshaling	マーシャリング
matching	マッチング
meaning	意味
meet	交わり
membership checking	所属性検査
meta-mathematics	メタ数学
metalanguage	メタ言語
metatheory	メタ理論
metavariables	メタ変数
method invocation	メソッド呼び出し
minimal type	最小型
mixfix	混置
modal logic	様相論理
model checker	モデル検査器
model checking	モデル検査
modular programming	モジュラープログラミング
modularity	モジュール性
module systems	モジュールシステム
module	モジュール
monad	モナド
monotone function	単調関数
monotype	単型
more general	より一般的（代入が）
most general unifier	最汎単一化子
μ-folding	μ畳み込み
μ-type	μ型
multi-method dispatch	多重メソッドディスパッチ
multi-method	マルチメソッド
multi-step evaluation	多ステップ評価
multiple inheritance	多重継承
mutable	書き換え可能な
nameless representation	名無し表現
nameless term	名無し項
naming context	名前付け文脈
narrowing	狭化
natural deduction	自然演繹
natural number	自然数
natural semantics	自然意味論
negative	負の
nested induction	多重帰納法
nominal type system	名前的型システム
non-strict	非正格な
normal form	正規形
normal order	正規順序
normalizable	正規化可能
normalization by evaluation	評価による正規化
normalization	正規化
notation	記法/表記
notation	表記/記法
numeric value	数値
object calculus	オブジェクト計算
object constructor	オブジェクトコンストラクタ
object identity	オブジェクト同一性
object language	対象言語
object-oriented	オブジェクト指向
object	オブジェクト
occur check	出現検査
open recursion	オープンな再帰
operational semantics	操作的意味論
optional value	オプション値
ordered set	順序集合
overloading	オーバーロード
override	オーバーライド
package	パッケージ
pair	二つ組
parallel reduction	並行簡約
parameter/argument	引数
parameter	パラメータ
parametric polymorphism	パラメータ多相
parametricity	パラメータ性
parser	構文解析器
partial equivalence relation	部分同値関係
partial evaluation	部分評価
partial function	部分関数
partial order	半順序
partial type reconstruction	部分的型再構築
partially abstract type	半抽象型
pattern matching	パターンマッチ
pattern typing	パターン型付け
pattern	パターン
permutation	並べ替え
π-calculus	π計算
pointer arithmetic	ポインタ算術
pointwise	各要素・各引数での
polarity	極性
polymorphic (record) update	多相（レコード）更新
polymorphic identity function	多相恒等関数
polymorphic lambda-calculus	多相ラムダ計算
polymorphic recursion	多相再帰
polymorphic repacking	多相再パッケージ化
polymorphic	多相的な
polymorphism	多相性
polytype	多型
positive subtyping	正の部分型付け
positive	正の
power kind	冪カインド
power type	冪型
powerset	冪集合
precedence	優先順位
predecessor	前者関数
predecessor	前者値
predicate	述語
predicative	可述的
prenex polymorphism	冠頭多相
preorder	前順序
preorder	前順序
preservation	保存
pretty printing	整形表示
principal solution	主要解
principal type	主要型
principal typing	主要型付け
principal unifier	主要単一化子
principle of safe substitution	安全代入の原則
procedural abstraction	手続きによる抽象化
process	プロセス
product	直積
progress	進行
promote	昇格する（型を）
proof theory	証明論
proper type	真の型
propositions as types	命題＝型
pure lambda-calculus	純粋なラムダ計算
pure type system (PTS)	純粋型システム
pure	純粋な
purely functional	純粋関数的
qualified type	限定型
raise	送出する（例外を）
ramified theory of types	分岐階型理論
range	値域
raw μ-types	生のμ型
reachable	到達可能
record kind	レコードのカインド
record	レコード
recursive type	再帰型
redex	簡約基
reducible candidate	簡約可能候補
reduction	簡約
reference	参照
refinement type	詳細型
reflection	リフレクション
reflexive and transitive closure	反射的推移的閉包
reflexive closure	反射的閉包
reflexive	反射的
region inference	リージョン推論
regular type	正則型
relation	関係
representation independence	表現非依存性
representation type	表現型
representation	表現
row kind	列カインド
row variable	列変数
row-variable polymorphism	列変数多相
rule schema	規則のスキーマ
run-time code generation	実行時コード生成
run-time error	実行時エラー
run-time monitoring	実行時モニタリング
run-time type error	実行時型エラー
safety	安全性
satisfy	充足する
saturated set	飽和集合
scope	スコープ
second-order lambda-calculus	二階ラムダ計算
semantic domain	意味領域
semantics	意味論
semi-unification	半単一化
sequence	列
sequencing	逐次実行
shape type	シェイプ型
shared state	共有状態
sharing	シェアリング
shifting	シフト
side condition	付帯条件
side effect	副作用
simple theory of types	単純階型理論
simple type	単純型
simply typed lambda-calculus	単純型付きラムダ計算
singleton kind	一元カインド
size	サイズ
small-step evaluation	小ステップ評価
small-step operational semantics	小ステップ操作的意味論
sound	健全
stack	スタック
state type	状態型（オブジェクトの）
state	状態
static distance	静的距離
store location	ストアでの位置
store typing	ストア型付け
store	ストア
stratified	階層化されている
strengthening	強化
strict	正格
strong binary operation	強二項演算
strong normalization	強正規化
structural induction	構造的帰納法
structural operational semantics	構造的操作的意味論
structural type system	構造的型システム
structural unfolding	構造的展開
stuck (state)	行き詰まり（状態）
stupid cast	愚かなキャスト
subclass	サブクラス
subject evaluation	主部評価
subject expansion	主部展開
subject reduction	主部簡約
subset semantics	部分集合意味論
substitution lemma	代入補題
substitution	代入
subsumption	包摂
subtree	部分木
subtype polymorphism	部分型多相
subtype	部分型
subtyping constraint	部分型付け制約
subtyping derivation	部分型付け導出
subtyping statement	部分型付け判断式
subtyping	部分型付け
successor	後者関数
successor	後者値
sum type	和型
superclass	スーパークラス
supertype	上位型
support function	支持関数
support graph	支持グラフ
surface syntax	表層構文
symmetric	対称的
syntactic control of interference	構文による干渉の制御
syntactic sugar	糖衣構文
syntax directed	構文主導
tag-free garbage collection	タグなしガベージコレクション
tagging	タグ付け
tail call	末尾呼び出し
tail-recursive	末尾再帰
term variable	項変数
term	項
termination measure	停止尺度
test	判定
threading	直列的に受け渡し
thunk	サンク
token	トークン
total function	全域関数
total order	全順序
transition function	遷移関数
transitive closure	推移的閉包
transitive	推移的
tree type	木型
tuple	組
typable	型付け可能
type abstraction	型抽象
type annotation	型注釈
type application	型適用
type ascription	型指定
type class	型クラス
type constructor	型構築子
type destructor	型分解子
type environment	型環境
type equivalence	型等価性
type erasure	型消去
type exposure	型露出
type inference	型推論
type name	型名
type operator	型演算子
type reconstruction	型再構築
type scheme	型スキーム
type substitution	型代入
type system	型システム
type tag	型タグ
type theory	型理論
type variable	型変数
type-assignment system	型割り当て体系
type-directed partial evaluation	型主導部分評価
type-passing semantics	型渡し意味論
type	型
typechecking	型検査
typing context	型付け文脈
typing derivation	型付け導出
typing relation	型付け関係
typing rule	型付け規則
typing statement	型付け判断式
typing	型付け
unboxed	アンボックス化された
uniform	一様
unify	単一化する
uninterpreted base type	非解釈の基本型
union type	合併型
universal domain	普遍領域
universal quantifier	全称量化子
universal set	普遍集合
universal type	全称型
unknown base type	未知の基本型
untyped	型無し
upcast	アップキャスト
value restriction	値制限
value	値
variable capture	変数捕獲
variable	変数
variance	変性
variant type	バリアント型
variant	バリアント
weak binary operation	弱二項演算
weak head reduction	弱頭部簡約
weak pointer	弱いポインタ
weak type variable	弱型変数
weakening	弱化
weight	重み
well behaved	よく振る舞う
well formed	正しい形式を持つ
well founded	整礎（順序が/集合が）
well typed	正しく型付けされている
width subtyping	幅部分型付け
wildcard binder	ワイルドカード束縛子
witness type	証人型