(*
Autor(s):
Andrej Dudenhefner (1)
Affiliation(s):
(1) Saarland University, Saarbrücken, Germany
*)
(*
Problem(s):
Simple Semi-Thue System 01 Rewriting (SSTS01)
*)
(*
Literature:
1 Dudenhefner, Andrej, and Jakob Rehof.
"Undecidability of Intersection Type Inhabitation at Rank 3 and its Formalization."
Fundamenta Informaticae 170.1-3 (2019): 93-110.
*)
Require Import List Relation_Operators.
(* A simple semi-Thue system consists of rules "ab -> cd" where a, b, c, d : nat *)
Definition Ssts := list ((nat * nat) * (nat * nat)).
(* one-step rewriting relation
if (ab -> cd) in ssts, then uabv -> ucdv where u, v : list nat *)
Inductive step (ssts: Ssts) : list nat -> list nat -> Prop :=
| step_intro {u v: list nat} {a b c d: nat} :
In ((a, b), (c, d)) ssts -> step ssts (u ++ a :: b :: v) (u ++ c :: d :: v).
(* reflexive, transitive closure of one-step rewriting *)
Definition multi_step (ssts: Ssts) : list nat -> list nat -> Prop :=
clos_refl_trans (list nat) (step ssts).
(* simple semi-Thue system 01 rewriting, that is
for given a simple semi-Thue system, does 0^(1+n) ->> 1^(1+n) hold for some n? *)
Definition SSTS01 : Ssts -> Prop :=
fun ssts => exists n, multi_step ssts (repeat 0 (1+n)) (repeat 1 (1+n)).
Autor(s):
Andrej Dudenhefner (1)
Affiliation(s):
(1) Saarland University, Saarbrücken, Germany
*)
(*
Problem(s):
Simple Semi-Thue System 01 Rewriting (SSTS01)
*)
(*
Literature:
1 Dudenhefner, Andrej, and Jakob Rehof.
"Undecidability of Intersection Type Inhabitation at Rank 3 and its Formalization."
Fundamenta Informaticae 170.1-3 (2019): 93-110.
*)
Require Import List Relation_Operators.
(* A simple semi-Thue system consists of rules "ab -> cd" where a, b, c, d : nat *)
Definition Ssts := list ((nat * nat) * (nat * nat)).
(* one-step rewriting relation
if (ab -> cd) in ssts, then uabv -> ucdv where u, v : list nat *)
Inductive step (ssts: Ssts) : list nat -> list nat -> Prop :=
| step_intro {u v: list nat} {a b c d: nat} :
In ((a, b), (c, d)) ssts -> step ssts (u ++ a :: b :: v) (u ++ c :: d :: v).
(* reflexive, transitive closure of one-step rewriting *)
Definition multi_step (ssts: Ssts) : list nat -> list nat -> Prop :=
clos_refl_trans (list nat) (step ssts).
(* simple semi-Thue system 01 rewriting, that is
for given a simple semi-Thue system, does 0^(1+n) ->> 1^(1+n) hold for some n? *)
Definition SSTS01 : Ssts -> Prop :=
fun ssts => exists n, multi_step ssts (repeat 0 (1+n)) (repeat 1 (1+n)).