(**************************************************************)
(* Copyright Dominique Larchey-Wendling * *)
(* *)
(* * Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(**************************************************************)
Require Import List Arith Lia.
From Undecidability.Shared.Libs.DLW.Vec
Require Import pos vec.
From Undecidability.TRAKHTENBROT
Require Import notations.
Set Implicit Arguments.
(* Copyright Dominique Larchey-Wendling * *)
(* *)
(* * Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(**************************************************************)
Require Import List Arith Lia.
From Undecidability.Shared.Libs.DLW.Vec
Require Import pos vec.
From Undecidability.TRAKHTENBROT
Require Import notations.
Set Implicit Arguments.
Record fo_signature := Mk_fo_signature {
syms : Type;
rels : Type;
ar_syms : syms -> nat;
ar_rels : rels -> nat
}.
Only one relational symbol of arity n
Definition Σrel (n : nat) : fo_signature.
Proof.
exists Empty_set (* No function or constant symbols *)
unit (* And one n-ary relational symbol *)
.
+ intros []. (* Value does not matter here *)
+ exact (fun _ => n). (* The n-ary relation *)
Defined.
One relational symbol of arity n and (interpreted) equality
Definition Σrel_eq (n : nat) : fo_signature.
Proof.
exists Empty_set (* No function or constant symbols *)
bool (* One ternary and equality *)
.
+ intros []. (* Value does not matter here *)
+ exact (fun b => if b then n else 2).
Defined.
The signature for the encoding of the binary
Post correspondance problem BPCP
(* Σbpcp_bool _ is unary, the two others are constants *)
Inductive Σbpcp_syms :=
| Σbpcp_bool : bool -> Σbpcp_syms (* shortcut is fb _ *)
| Σbpcp_unit : Σbpcp_syms (* shortcut is fe *)
| Σbpcp_undef : Σbpcp_syms (* shortcut is *)
.
(* all these are binary symbols *)
Inductive Σbpcp_rels :=
| Σbpcp_hand : Σbpcp_rels (* shortcut is p_P *)
| Σbpcp_ssfx : Σbpcp_rels (* shortcut is p_lt *)
| Σbpcp_eq : Σbpcp_rels (* shortcut is p_eq *)
.
Definition Σbpcp : fo_signature.
Proof.
exists Σbpcp_syms Σbpcp_rels.
+ exact (fun s =>
match s with
| Σbpcp_bool _ => 1
| _ => 0
end).
+ exact (fun _ => 2).
Defined.
Semantics: FO models
Record fo_model Σ (X : Type) := Mk_fo_model {
fom_syms : forall s, vec X (ar_syms Σ s) -> X;
fom_rels : forall r, vec X (ar_rels Σ r) -> Prop }.
FO model decidability/computability
Definition fo_model_dec Σ X (M : fo_model Σ X) :=
forall r (v : vec _ (ar_rels _ r)), { fom_rels M r v } + { ~ fom_rels M r v }.
FO model from a binary rel
Definition rel2_on_vec X (R : X -> X -> Prop) (v : vec X 2) : Prop :=
R (vec_head v) (vec_head (vec_tail v)).
Arguments rel2_on_vec {X} R v /.
Section bin_rel_Σ2.
Variable (X : Type) (R : X -> X -> Prop).
Definition bin_rel_Σ2 : fo_model (Σrel 2) X.
Proof.
exists; intros [].
exact (rel2_on_vec R).
Defined.
Hypothesis HR : forall x y, { R x y } + { ~ R x y }.
Fact bin_rel_Σ2_dec : fo_model_dec bin_rel_Σ2.
Proof. intros [] v; apply HR. Qed.
End bin_rel_Σ2.