erutuf

module NeuralNetwork where

import Data.List
import System.Random
import Control.Monad
import Numeric.LinearAlgebra

learnCnst = 0.01

addThres v = vector $ toList v ++ [1.0]

erutuf

\ProvidesPackage{beamerthemeErutuf}
\mode<presentation>

%% font size
\setbeamerfont{title}{parent=structure,size=\Large}
\setbeamerfont{section in head/foot}{size=\tiny,series=\bfseries}
\setbeamerfont{frametitle}{parent=structure,size=\Large,series=\bfseries}
\setbeamerfont{framesubtitle}{parent=frametitle,size=\large}
\setbeamerfont{itemize/enumerate body}{size=\normalsize}
\setbeamerfont{itemize/enumerate subbody}{size=\small}

erutuf

Risa/Asir で D 加群の積分を計算

Risa/Asir

オープンソースの数式処理システム

http://www.math.kobe-u.ac.jp/Asir/asir-ja.html

ここからダウンロード&インストール

erutuf

(* sample code of automatic differentiation in Coq *)

Require Import QArith.
Open Scope Q_scope.

Definition QFunc := Q -> Q.

Parameter der_rel : QFunc -> QFunc -> Prop.

Axiom add_der : forall f g f' g', der_rel f f' -> der_rel g g' ->

erutuf

(* sample code of automatic differentiation in Coq *)

Require Import QArith.
Open Scope Q_scope.

Definition QFunc := Q -> Q.

Parameter der_rel : QFunc -> QFunc -> Prop.

Axiom add_der : forall f g f' g', der_rel f f' -> der_rel g g' ->

erutuf

Add LoadPath "/Users/erutuf/Documents/mit/fiat/src" as Fiat.
Require Import Fiat.Common Fiat.Computation
  Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements.
Require Import List Omega.

Set Implicit Arguments.
Set Regular Subst Tactic.
Import ListNotations.

Inductive removed A : nat -> list A -> list A -> Prop :=

erutuf

Require Import List.
Import ListNotations.

Inductive State := Q1 | Q2.
Inductive Alphabet := A | B.

Inductive trans : State -> Alphabet -> State -> Prop :=
| tr1A : trans Q1 A Q2
| tr1B : trans Q1 B Q1
| tr2A : trans Q2 A Q1

erutuf

Require Import List.
Import ListNotations.

Definition Board := list (list nat).

Definition size (board : Board) := length board.

Definition val (n m : nat)(board : Board) := nth m (nth n board []) 1.

Fixpoint fill' m (l : list nat) : list nat :=

erutuf

let rec find quot node =
  if quot.(node) = node
  then node
  else
    let repr = find quot quot.(node) in
    quot.(node) <- repr;
    repr

let union quot node1 node2 =

erutuf

Require Import List.
Import ListNotations.

Set Implicit Arguments.

(* begin hide *)

Definition is_true x := x = true.

Coercion is_true : bool >-> Sortclass.