As written (and with a definition provided for max_distance), your script works
fine. Your error message must be for some other problem.
From your description, it sounds as if you want to use MAP to alter all ch
values in a pop (which is a chromosome list).
As it seems very computational, I’d recommend trying to write your algorithm in
SML (or Haskell, or OCaml), and then translating it to HOL.
Michael
From: 幻＠未来 <849678...@qq.com>
Date: Thursday, 20 December 2018 at 12:38
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] Element assignment in structures
The following data types are defined in HOL4.
val _ = Datatype `
coordinate = <|
x_axis: real;
y_axis: real;
z_axis: real
|> `;
val _ = Datatype `
chromosome = <|
r: num;
b: num;
distance: real;
rx: coordinate;
path: coordinate list;
bx: coordinate
|> `;
val ch = ``ch: chromosome``;
val pop = ``pop: chromosome list``;
val get_def = Define `
get pop ch = if MEM ch pop then (ch with <| distance :=
ch.distance + max_distance pop |>)
else (ch with <| distance := ch.distance |>)`;
val get1_def = Define `
get1 pop = !ch. if MEM ch pop then (ch.distance = ch.distance +
max_distance pop)
else ch.distance = ch.distance`;
The definition of get_def is successful, but the definition of get1_def is
unsuccessful. Defining get1_def will report an error:
Exception raised at Preterm.type-analysis:
roughly between line 878, character 19 and line 879, character 58:
Type inference failure: unable to infer a type for the application of
($! :(α -> bool) -> bool) :(α -> bool) -> bool
on line 878, characters 14-17
to
λ(ch :chromosome).
if MEM ch (pop :chromosome list) then
ch with distance := ch.distance + max_distance pop
else ch with distance := ch.distance
roughly between line 878, character 19 and line 879, character 58
which has type
:chromosome -> chromosome
unification failure message: Attempt to unify different type operators:
min$bool and scratch$chromosome
What I want to do is to give a pop(:chromosome list), for any
ch(:chromosome) in the pop , if some conditions are met, then the distance
value in ch is modified. How to solve this problem?
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
