MLCore

A small machine-learning API whose safety properties live in Aeon's types. The Python binding only reads data and delegates splitting, fitting, and scoring to pandas/scikit-learn. Linearity, valid arguments, compatibility, provenance, and result bounds are checked statically from this interface. For general tabular ETL / column kernels, prefer ``DataFrame.ae`` (pandas + ``Array`` bridge). This module keeps a ML-specialized linear ``DataFrame`` with ``df_rows`` / ``df_cols`` measures for the toy decision-tree pipeline.
Table of Contents

Types

DataFrame

(type) linear
linear type DataFrame

Dataset

(type) linear
linear type Dataset

DatasetSplit

(type) linear
linear type DatasetSplit

TrainingDataset

(type) linear
linear type TrainingDataset

TestingDataset

(type) linear
linear type TestingDataset

DecisionTreeClassifier

(type)
type DecisionTreeClassifier

Functions

read_csv

CSV shape is supplied as logical metadata. The expected values are used by the refinement checker but deliberately omitted from the native expression, so the Python binding remains a thin call to pandas.read_csv.
def read_csv (path : String) (expected_rows : Int | expected_rows ≥ 0) (expected_columns : Int | expected_columns ≥ 1) : {df : DataFrame | df_rows df = expected_rows && df_cols df = expected_columns}

target

Select a zero-based target column. The input must be known to contain both a target and at least one feature. DataFrame is linear, so target consumes it.
def target (1 df : DataFrame | df_cols df ≥ 2) (column : Int | 0 ≤ column && column < df_cols df) : {ds : Dataset | ds_rows ds = df_rows df && (ds_features ds = df_cols df - 1 && ds_features ds ≥ 1)}

split

The fraction is checked statically. The native implementation performs a deterministic stratified split but contains no duplicate argument checks.
def split (1 ds : Dataset | ds_features ds ≥ 1) (train_size : Float | 0.0 < train_size && train_size < 1.0) : {parts : DatasetSplit | split_features parts = ds_features ds}

consume_split

Eliminate a split once and expose its two distinct linear halves. The callback type relates their feature count and logical split provenance.
def consume_split (1 parts : DatasetSplit) ( 1 consumer : ( 1 training : TrainingDataset | training_rows training > 0 && ( training_features training ≥ 1 && (training_features training = split_features parts && training_split_id training = split_provenance parts) ) ) → ( 1 testing : TestingDataset | testing_rows testing > 0 && (testing_features testing = training_features training && testing_split_id testing = split_provenance parts) ) → result ) : result

decision_tree_classifier

Training consumes the training half and records its static metadata in the model type. No provenance or schema fields are attached to the Python object.
def decision_tree_classifier (1 training : TrainingDataset) : { model : DecisionTreeClassifier | classifier_features model = training_features training && classifier_split_id model = training_split_id training }

accuracy

Evaluation consumes a compatible held-out test half. Feature count and split provenance are checked statically; the result contract proves that accuracy is bounded without a Python range check.
def accuracy (model : DecisionTreeClassifier) ( 1 testing : TestingDataset | testing_features testing = classifier_features model && testing_split_id testing = classifier_split_id model ) : {score : Float | 0.0 ≤ score && score ≤ 1.0}

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

df_rows

uninterpreted
Logical metadata used exclusively by the refinement checker.
def df_rows : (df : DataFrame) → Int

df_cols

uninterpreted
def df_cols : (df : DataFrame) → Int

ds_rows

uninterpreted
def ds_rows : (ds : Dataset) → Int

ds_features

uninterpreted
def ds_features : (ds : Dataset) → Int

split_features

uninterpreted
def split_features : (parts : DatasetSplit) → Int

split_provenance

uninterpreted
def split_provenance : (parts : DatasetSplit) → Int

training_rows

uninterpreted
def training_rows : (ds : TrainingDataset) → Int

training_features

uninterpreted
def training_features : (ds : TrainingDataset) → Int

training_split_id

uninterpreted
def training_split_id : (ds : TrainingDataset) → Int

testing_rows

uninterpreted
def testing_rows : (ds : TestingDataset) → Int

testing_features

uninterpreted
def testing_features : (ds : TestingDataset) → Int

testing_split_id

uninterpreted
def testing_split_id : (ds : TestingDataset) → Int

classifier_features

uninterpreted
def classifier_features : (model : DecisionTreeClassifier) → Int

classifier_split_id

uninterpreted
def classifier_split_id : (model : DecisionTreeClassifier) → Int