ボキャブラリーとコンテキスト

指標による定義:

module TransitionSystem

signture RightTransitionSystem within (C in MonCAT} {
  sort A
  sort S
  operation t: S×A → S

  alias alphabet := A
  alias state-space := S
  alias right-transition := t
  alias transition := right-transition
}

alias TransitionSystem := RightTransitionSystem

signature DetTransitionSystem := TransitionSystem within Set
signature ParTransitionSystem := TransitionSystem within Partial
signature NonDetTransitionSystem := TransitionSystem within NonDet

continue

標準的なボキャブラリーとコンテキスト:

vocabulary TransitionSystem for module TransitionSystem {
  RightTransitionSystem
  RightTransitionSystem.A
  RightTransitionSystem.S
  RightTransitionSystem.t
  DetTransitionSystem
  ParTransitionSystem
  NonDetTransitionSystem
}

context StdAlias for vocabulary TransitionSystem {
  TransitionSystem := RightTransitionSystem
  TransitionSystem.alphabet := RightTransitionSystem.A
  TransitionSystem.state-space := RightTransitionSystem.S
  TransitionSystem.right-transition := RightTransitionSystem.t
  TransitionSystem.transition := RightTransitionSystem.t
}

context 日本語標準 for context StdAlias {
  遷移系 := TransitionSystem
  遷移系のアルファベット := TransitionSystem.alphabet 
  遷移系の状態空間 := TransitionSystem.state-space
  遷移系の右遷移 := TransitionSystem.right-transition
  遷移系の遷移 := TransitionSystem.transition
}

追加:

module TransitionSystem

signture TransitionSystemMisc extends TransitionSystem within (C in CartCat) {
  operation a: 1 → A
  operation s: 1  → S

  alias action-label := a
  alias state-point := s
}

end
vocabulary TransitionSystemMisc for module TransitionSystem {
  action-label := TransitionSystemMisc.a
  state-point := TransitionSystemMisc.s
}

context 日本語追加 for vocabulary TransitionSystemMisc {
  アクションラベル := action-label
  状態点 := state-point
}

別名:

context 日本語別名-1 for context 日本語標準 {
  {状態}?{遷移}?{マシン | エンジン} := 遷移系
  {遷移系 | {状態}?{遷移}?{マシン | エンジン}}の{実行 | 作用} := 遷移系の遷移
}

context 日本語別名-2 for context 日本語追加 {
  {{アクション | 入力 | 刺激}?{ラベル | レター | 記号 | シンボル | 信号} | インストラクション{記号 | ラベル | ニモニック}? := アクションラベル
  状態 := 状態点
}