Stream: Beginner Questions

Topic: Clash of types error in a definition of a construction

Atie Bastan (Dec 11 2024 at 05:32):

I am reproducing this proof with minor alterations:
https://www.isa-afp.org/sessions/finite_automata_hf/#Finite_Automata_HF.html

However, when I get to this definition, I get a clash of types error :

definition Power_dfa :: " 'a dfa" where
  "Power_dfa = ⦇dfa.states = {AX (epsclo q) | q. q ∈ Pow (states N)},
                     init  = AX (epsclo (init N)),
                     final = {AX (epsclo Q) | Q. Q ⊆ states N ∧ Q ∩ final N ≠ {}},
                     nxt   =λQ x. AX(⋃q ∈ epsclo Q. epsclo (nxt N q x)) ⦈"

The error is:

Type unification failed: Clash of types "_ set" and "nat"

Type error in application: incompatible operand type

Operator:
FAHS.dfa.dfa_ext
{AX (epsclo q) |q. q ∈ Pow (FAHS.nfa.states N)}
(AX (epsclo (FAHS.nfa.init N)))
{AX (epsclo Q) |Q.
Q ⊆ FAHS.nfa.states N ∧
Q ∩ FAHS.nfa.final N ≠ {}} ::
(nat ⇒ ??'a ⇒ nat)
⇒ ??'b ⇒ (??'a, ??'b) FAHS.dfa_scheme
Operand:
λQ x. AX (⋃q∈epsclo Q.
epsclo (FAHS.nfa.nxt N q x)) ::
nat set ⇒ 'a ⇒ nat

This is the kind of alterations i am making to the original proof:

record 'a  dfa =
                states :: "nat set"
                init   :: "nat"
                final  :: "nat set"
                nxt    :: "nat ⇒ 'a ⇒ nat"


record  'a nfa = states :: "nat set"
                init   :: "nat set"
                final  :: "nat set"
                nxt    :: "nat ⇒ 'a ⇒ nat set"
                eps    :: "(nat × nat) set"

definition AX :: "nat set ⇒ nat"
  where "AX A = set_encode (A)"

Mathias Fleury (Dec 11 2024 at 06:00):

And your question is what?

Mathias Fleury (Dec 11 2024 at 06:01):

The error message is saying that you apply the term FAHS.dfa.dfa_ext {AX (epsclo q) |q. q ∈ Pow (FAHS.nfa.states N)} (AX (epsclo (FAHS.nfa.init N))) {AX (epsclo Q) |Q. Q ⊆ FAHS.nfa.states N ∧ Q ∩ FAHS.nfa.final N ≠ {}}
with is expecting an argument with type

nat ⇒ ??'a ⇒ nat

but the argument λQ x. AX (⋃q∈epsclo Q. epsclo (FAHS.nfa.nxt N q x)) has type

nat set ⇒ 'a ⇒ nat

Mathias Fleury (Dec 11 2024 at 06:02):

And nat and nat set cannot be unified

Mathias Fleury (Dec 11 2024 at 06:02):

But all that is written in the error message

Mathias Fleury (Dec 11 2024 at 06:04):

λQ x. AX (⋃q∈epsclo Q. epsclo (FAHS.nfa.nxt N q x)) is your nxt if you did not recognize it

Atie Bastan (Dec 11 2024 at 19:38):

I am trying to define a function that prepares the input for dfa.nxt in the correct format it requires. This function takes a nat set, but returns a nat, the proper type for the dfa.nxt.
If this is not an appropriate way to say this, how should i do this?

Mathias Fleury (Dec 11 2024 at 19:50):

1. currently you have defined nxt :: "nat ⇒ 'a ⇒ nat set". This is your definition of nxt. By definition you have to respect the type everywhere
2. in your definition you are trying to use nat set => 'a => nat set. This is not compatible with the definition in 1

Mathias Fleury (Dec 11 2024 at 19:51):

We cannot tell you if :

1. you need to change the definition to allow for nat set
2. you have an incorrect definition
3. something else I am not seeing

Atie Bastan (Dec 11 2024 at 23:53):

Thank you! This helped me significantly.

Last updated: Dec 21 2024 at 16:20 UTC