型理論
• ラッセルのパラドックス：
「集合の集合」は矛盾を引き起こす。
ラッセル、ホワイトヘッド
「プリンキピアマセマティカ」
• プログラミング言語のコンパイル時チェック
型つきl計算
型
Type::= BaseType | Type → Type | Type ×Type
BaseType ::=a | b | …
(基底型は型)
l項
Var ::= v | Var ’
Term ::= Var | (Term Term) | (l Var:Type. Term)
| < Term, Term>
略記法は型なしと同様
型判定
• 型判定式
• 型推論法則
  M :
  x : 　( x : は に含まれる )
  M :   　  N : 
  MN : 
, x :   M : 
  lx :  .M :   
  M : 　  N : 
  M , N :   
  N :     N :  
,
  fst ( N ) :    snd ( N ) : 
breduction
, x :   M : 　  N : 
  (lx :  .M ) N  M [ x : N ] : 
構成的プログラミング
型を命題と考え,
を 
を 
と解釈すれば(Curry-Howard Isomorphism) 、
型つきλ項は述語論理の証明。
• 自動証明器にかければ自動的にプログラムができ
る？
Martin-Lof, P. : Constructive mathematics and computer programming, in Logic,
Methodology, and Philosophy of Science IV, Cohen, L. J. et al. eds., NorthHolland(1982), pp.153-179.
型つきl計算の性質
• 無限の長さのb簡約列は存在しない
（強正規化可能）
計算が必ず止まる
• 不動点演算子が存在しない
GUIにあらわれる関数概念
• 例示によるプログラミング
(Programming by Demonstration, PBD)
• 作業の再帰定義
• (Rule-Based) Visual Languages
Dependency Tree
Data Structure
Fixpoint Operator
on Dependency Tree
Fixpoint figure and its
semantics
＝
Fix/3:
fixpoint figure of arity 3

「 YG 性格検査 実施方法 」講習会 - 竹井機器工業

「 YG 性格検査 実施方法 」講習会